diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-04 08:39:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-04 08:39:56 +0000 |
| commit | a3397a0cdd8af9f9cde954b3647a45476df91439 (patch) | |
| tree | e1fd96ca46c45da16b2c2b6877911eea37cae620 /isar | |
| parent | 2caea10ae59fa63882ed60cb92a6d4250832e0ba (diff) | |
Remove proof-no-command
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar-syntax.el | 2 | ||||
| -rw-r--r-- | isar/isar.el | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 3cf66850..1af9e545 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -461,7 +461,7 @@ matches contents of quotes for quoted identifiers.") (defun isar-undos (i) (if (> i 0) (concat "undos_proof " (int-to-string i) ";") - proof-no-command)) + nil)) ; was proof-no-command (defun isar-cannot-undo (cmd) (concat "cannot_undo \"" cmd "\";")) diff --git a/isar/isar.el b/isar/isar.el index 5014fc9b..bfe635d0 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -456,7 +456,8 @@ This is called when Proof General spots output matching (setq ans isar-undo))) (if ans (setq answers (cons ans answers))) (if span (setq span (next-span span 'type)))) - (if (null answers) proof-no-command (apply 'concat answers)))) + (if (null answers) nil ; was proof-no-command + (apply 'concat answers)))) (defun isar-goal-command-p (span) "Decide whether argument SPAN is a goal or not." |