aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar-keywords.el
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2000-06-03 22:12:32 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2000-06-03 22:12:32 +0000
commit70f99119285a02089b32c54c758e2d8a59680a71 (patch)
tree01ad892e9bf44087d065a299d2d21da3fd132e55 /isar/isar-keywords.el
parent412c63386bab6e2be010ae02c6017561e56bc591 (diff)
{ } are back;
Diffstat (limited to 'isar/isar-keywords.el')
-rw-r--r--isar/isar-keywords.el7
1 files changed, 2 insertions, 5 deletions
diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index 520ad80f..f2d180a1 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -149,11 +149,8 @@
"use_thy_only"
"welcome"
"with"
- ;; FIXME da: commented out these since {* *} appear after start of
- ;; command, e.g. header {* blah *} etc, which breaks
- ;; proof-script-command-start-regexp
- ;; "{"
- ;; "}"
+ "{"
+ "}"
))
(defconst isar-keywords-minor