aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar.el
diff options
context:
space:
mode:
Diffstat (limited to 'isar/isar.el')
-rw-r--r--isar/isar.el9
1 files changed, 1 insertions, 8 deletions
diff --git a/isar/isar.el b/isar/isar.el
index f75ff2a9..ba119531 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -97,16 +97,9 @@ See -k option for Isabelle interface script."
;; proof script syntax
proof-terminal-char ?\; ; forcibly ends a command
proof-electric-terminator-noterminator t ; don't insert it
- proof-script-command-start-regexp
- (proof-regexp-alt
- ;; FIXME: this gets { and } wrong: they must _not_ appear as {* *}
- ;; because that's lexically a kind of comment.
- isar-any-command-regexp
- (regexp-quote ";"))
+ proof-script-command-start-regexp isar-any-command-regexp
proof-script-integral-proofs t
- ;; FIXME: use old parser for now to avoid { } problem
- proof-script-use-old-parser t
proof-script-comment-start isar-comment-start
proof-script-comment-end isar-comment-end
proof-script-comment-start-regexp isar-comment-start-regexp