From c666c280b3c8204226be7cc8b89c24095decd851 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 10 Sep 2009 23:52:08 +0000 Subject: Disable debug message in Isar --- generic/proof-script.el | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'generic/proof-script.el') 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) -- cgit v1.2.3