diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-11-23 23:25:11 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-11-23 23:25:11 +0000 |
| commit | aa9bd33b1850e8743d57e12e006297eda3d66100 (patch) | |
| tree | b2155326d93ee89721dd2b69bef13886b4f749f6 /isar/isar-syntax.el | |
| parent | 95522c91b0773c7726ea4cac75270a9396e654cd (diff) | |
Use ProofGeneral.pr if available. See Trac #292.
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 958f4558..408b910e 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -447,13 +447,24 @@ matches contents of quotes for quoted identifiers.") (defconst isar-undo "ProofGeneral.undo;") +(defun isar-pr () + (if (member "ProofGeneral\\.pr" + isar-keywords-major) + "ProofGeneral.pr" ; does right thing + "pr" ; See Trac #292 + )) + (defun isar-remove (name) (concat "init_toplevel; kill_thy " name ";")) (defun isar-undos (linearp i) (if (> i 0) (concat (if linearp "linear_undo " "undos_proof ") (int-to-string i) ";" - (if linearp " pr; ")) ; See Trac #292 + (if linearp + (concat " " + (isar-pr) + ";")) + ) nil)) ; was proof-no-command (defun isar-cannot-undo (cmd) |