diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 09:33:36 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 09:33:36 +0000 |
| commit | d5a0b9024ec59523d0744efdceda30adff2a7969 (patch) | |
| tree | 63baa0118abb6441be3c160eaadd8f355a02a093 /isar/isar.el | |
| parent | b2ab0c0ccc9637b6c467e65183653b4366854919 (diff) | |
Add proof-electric-terminator-noterminator behaviour for Isar
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/isar/isar.el b/isar/isar.el index 0fe23c21..2281f3f0 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -87,8 +87,10 @@ See -k option for Isabelle interface script." proof-prog-name-guess t ;; proof script syntax - proof-terminal-char ?\; ; forcibly ends a command + 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. |