From 595071c25dbdce4c793f35b4bf4beb0e1f5b1483 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sat, 3 Oct 2009 18:08:55 +0000 Subject: Start using new parser, adjusting isar-any-command-regexp. --- isar/isar.el | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'isar/isar.el') 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 -- cgit v1.2.3