diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-10-03 18:08:55 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-10-03 18:08:55 +0000 |
| commit | 595071c25dbdce4c793f35b4bf4beb0e1f5b1483 (patch) | |
| tree | b6c6d72ee313311646ccf26e4312dfe70520c3e2 /isar/isar.el | |
| parent | 7ffacf7b684ffb1d0df776c697019dc8027eb12c (diff) | |
Start using new parser, adjusting isar-any-command-regexp.
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 9 |
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 |