Comments.

2 files changed, 9 insertions, 1 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index a4d51f54..aa534a2e 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1637,6 +1637,9 @@ by the filter is to send the next command from the queue."
 ;; -- need to fontify remaining portion of buffer in case
 ;;   tracing output has ended when in slow mode (and refresh
 ;;   final display)  
+;; -- shouldn't be trigger for only a small amount of output 
+;;   (e.g. output from blast).  Or a count of number of succesive
+;;   bursts?
 
 (defvar pg-last-tracing-output-time nil
   "Time of last tracing output, as recorded by (current-time).")
@@ -1788,7 +1791,8 @@ Calls proof-state-change-hook."
 
 ;;;###autoload
 (defun proof-shell-invisible-command (cmd &optional wait)
-  "Send CMD to the proof process.  
+  "Send CMD to the proof process.
+The CMD is `invisible' in the sense that it is not recorded in buffer.
 CMD may be a string or a string-yielding function.
 Automatically add proof-terminal-char if necessary, examining
 proof-shell-no-auto-terminate-commands.
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 5c1c5f87..c7d9a1cb 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -574,6 +574,10 @@ No action if BUF is nil or killed."
 	 (if noselect
 	     ;; FIXME: would like 'norecord arg here to override
 	     ;; previous window entering top of MRU list here.
+	     ;; In fact, this could be hacked in XEmacs code.
+	     ;; GNU Emacs seems *not* to put previously displayed
+	     ;; window onto the top of the list with record-buffer:
+	     ;; that gives much nicer behaviour than XEmacs here.
 	     (display-buffer buf 'not-this-window)
 	   (let ((pop-up-windows t))
 	     (pg-pop-to-buffer buffer 'not-this-window 'norecord))))))