diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-09 23:13:01 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-09 23:13:01 +0000 |
| commit | 41542208cdf5437bf7604d042779d5ac9d7684a8 (patch) | |
| tree | 0e621d636eeea579ef82a605f1c4a3203a116034 /isar/isar-syntax.el | |
| parent | f1dc2bd435c9bb6442925b314198f312bc60c0ee (diff) | |
Support linear_undo. Add minimal font-lock for readability in *isabelle*.
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 2e024eac..83d879a5 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -418,6 +418,9 @@ matches contents of quotes for quoted identifiers.") "Remove invisible output markup from STRING" (replace-regexp-in-string "\^A." "" string)) +(defconst isar-shell-font-lock-keywords + '(("\^A." (0 '(face nil invisible t))))) + (defvar isar-goals-font-lock-keywords (append (list @@ -459,8 +462,9 @@ matches contents of quotes for quoted identifiers.") (defun isar-remove (name) (concat "init_toplevel; kill_thy " name ";")) -(defun isar-undos (i) - (if (> i 0) (concat "undos_proof " (int-to-string i) ";") +(defun isar-undos (linearp i) + (if (> i 0) (concat (if linearp "linear_undo " "undos_proof ") + (int-to-string i) ";") nil)) ; was proof-no-command (defun isar-cannot-undo (cmd) |