diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-10 23:52:08 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-10 23:52:08 +0000 |
| commit | c666c280b3c8204226be7cc8b89c24095decd851 (patch) | |
| tree | e7cac1787697cb41237fd5da87ee6b9c11440d1c /generic/proof-script.el | |
| parent | e1211216548239888f068f97b824945353d0b0f5 (diff) | |
Disable debug message in Isar
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 94e677df..fc0027c5 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1333,8 +1333,10 @@ Argument SPAN has just been processed." (defun proof-done-advancing-save (span) "A subroutine of `proof-done-advancing'. Add info for save span SPAN." - (unless (eq proof-shell-proof-completed 1) + (unless (or (eq proof-shell-proof-completed 1) + (eq proof-assistant-symbol 'isar)) ;; We expect saves to succeed only for recently completed top-level proofs. + ;; NB: not true in Isar, because save commands can perform proof. (proof-debug (format "PG: save command with proof-shell-proof-completed=%s, proof-nesting-depth=%s" @@ -1352,7 +1354,7 @@ Argument SPAN has just been processed." (and proof-save-with-hole-regexp (proof-string-match proof-save-with-hole-regexp cmd) ;; Give a message of a name if one can be determined - (message "%s" + (proof-minibuffer-message "proved %s" (setq nam (if (stringp proof-save-with-hole-result) (replace-match proof-save-with-hole-result nil nil cmd) |