diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-18 09:56:48 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-18 09:56:48 +0000 |
| commit | a4140dadd9931388b567fbb5bd2003f14641dea0 (patch) | |
| tree | a3c2941871a248269515ddf83cfdeca97c7e90f2 /isar/isar-syntax.el | |
| parent | eaded708c5fa1010120878a0172bd5ca1ec1efce (diff) | |
First attempt at command wrapping (see http://proofgeneral.inf.ed.ac.uk/trac/ticket/199)
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 0bc279f3..487a1bdc 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -13,7 +13,6 @@ (require 'proof-syntax) (require 'isar-keywords) - ;; ----- character syntax (defconst isar-script-syntax-table-entries @@ -467,6 +466,14 @@ matches contents of quotes for quoted identifiers.") (defun isar-cannot-undo (cmd) (concat "cannot_undo \"" cmd "\";")) +(defconst isar-undo-commands + (list + isar-linear-undo + isar-undo + "init_toplevel" "kill_thy" + "undos_proof" + "cannot_undo")) + (defconst isar-theory-start-regexp (proof-anchor-regexp (isar-ids-to-regexp |