diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-28 08:40:57 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-28 08:40:57 +0000 |
| commit | 4b2801a521f7365f8a3833fa9805828792dac853 (patch) | |
| tree | 1c9159ba41b75b362370307a098e3c86821dafcc /isar/isar.el | |
| parent | 07c7e94620921a826ac07363bf49f35cff0e6bc9 (diff) | |
Functions find-and-forget and count-undos now return lists of commands
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/isar/isar.el b/isar/isar.el index 6c58e1eb..f75ff2a9 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -434,7 +434,7 @@ This is called when Proof General spots output matching (setq i (+ 1 i)))) (t nil)))) (setq span (next-span span 'type))) - (isar-undos isar-use-linear-undo ct))) + (list (isar-undos isar-use-linear-undo ct)))) ;; undo theory commands (defun isar-find-and-forget (span) @@ -474,8 +474,7 @@ 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) nil ; was proof-no-command - (apply 'concat answers)))) + answers)) (defun isar-goal-command-p (span) "Decide whether argument SPAN is a goal or not." |