diff options
| author | Makarius Wenzel | 1999-05-25 08:09:49 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-05-25 08:09:49 +0000 |
| commit | 5e8e51f9a6d9b5e56ec5e918bdf6fdb90180ab9b (patch) | |
| tree | ea4c88b57cd090ad1cd13ec11ea6183f97e919d9 | |
| parent | c9a01104f2a4ad4d70ecfcdea50c7754efc9bd36 (diff) | |
tuned;
| -rw-r--r-- | isar/isar.el | 37 |
1 files changed, 18 insertions, 19 deletions
diff --git a/isar/isar.el b/isar/isar.el index 8c772c82..6e381d74 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -127,7 +127,7 @@ proof-kill-goal-command "kill_proof;" ;; command hooks proof-goal-command-p 'isar-goal-command-p - proof-global-save-command-p 'isar-global-save-command-p + proof-really-save-command-p 'isar-global-save-command-p proof-count-undos-fn 'isar-count-undos proof-find-and-forget-fn 'isar-find-and-forget proof-goal-hyp-fn 'isar-goal-hyp @@ -467,24 +467,23 @@ Resulting output from Isabelle will be parsed by Proof General." (defun isar-global-save-command-p (span str) "Decide whether argument really is a global save command" - (and (proof-string-match isar-save-command-regexp str) - (let ((ans nil) (lev 0) cmd) - (while (and span (not ans)) - (setq span (prev-span span 'type)) - (setq cmd (span-property span 'cmd)) - (cond - ;; comment: skip - ((eq (span-property span 'type) 'comment)) - ;; local qed: enter block - ((proof-string-match isar-save-command-regexp cmd) - (setq lev (+ lev 1))) - ;; local goal: leave block, or done - ((proof-string-match isar-local-goal-command-regexp cmd) - (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no))) - ;; global goal: done - ((proof-string-match isar-goal-command-regexp cmd) - (setq ans 'yes)))) - (eq ans 'yes)))) + (let ((ans nil) (lev 0) cmd) + (while (and span (not ans)) + (setq span (prev-span span 'type)) + (setq cmd (span-property span 'cmd)) + (cond + ;; comment: skip + ((eq (span-property span 'type) 'comment)) + ;; local qed: enter block + ((proof-string-match isar-save-command-regexp cmd) + (setq lev (+ lev 1))) + ;; local goal: leave block, or done + ((proof-string-match isar-local-goal-command-regexp cmd) + (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no))) + ;; global goal: done + ((proof-string-match isar-goal-command-regexp cmd) + (setq ans 'yes)))) + (eq ans 'yes))) (defvar isar-current-goal 1 "Last goal that emacs looked at.") |