Improve handling of intermittent fontification for trace buffers.

3 files changed, 35 insertions, 14 deletions

diff --git a/generic/pg-response.el b/generic/pg-response.el
index 9970e7fd..c8da307e 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -97,7 +97,8 @@ Internal variable, setting this will have no effect!")
     (modeline . nil)			; ignored?
     (unsplittable . t)
     (menu-bar-lines . 0)
-    (tool-bar-lines . nil))
+    (tool-bar-lines . nil)
+    (proofgeneral . t)) ;; indicates generated for/by PG  FIXME!!
   "List of GNU Emacs frame parameters for secondary frames.")
 
 (defun proof-multiple-frames-enable ()
@@ -446,33 +447,45 @@ See `pg-next-error-regexp'."
 
 (defvar proof-trace-last-fontify-pos nil)
 
+(defun proof-trace-fontify-pos ()
+  "Return the position to fontify from in the tracing buffer, if any."
+  (if proof-trace-last-fontify-pos
+      (if (> proof-trace-last-fontify-pos (point))
+	  (point-min);; in case buffer cleared
+	proof-trace-last-fontify-pos)))
+
 ;; An analogue of pg-response-display-with-face 
 (defun proof-trace-buffer-display (str)
-  "Output STR in the trace buffer.
-If STR is empty, just ensure that fontification is up to date."
+  "Output STR in the trace buffer, moving the pointer downwards.
+We fontify the output only if we're not too busy to do so."
   (with-current-buffer proof-trace-buffer
     (goto-char (point-max))
-    (unless (string-equal str "")
-      (newline))
+    (newline)
     (or proof-trace-last-fontify-pos 
 	(setq proof-trace-last-fontify-pos (point)))
     (insert str)
-    (unless (or (bolp) (string-equal str ""))
+    (unless (bolp)
       (newline))
     ;; If tracing output is prolific, we try to avoid
     ;; fontifying every chunk and batch it up instead.
     (unless pg-tracing-slow-mode
-      (let ((fontifystart (if (> proof-trace-last-fontify-pos (point))
-			      (point-min);; in case buffer cleared
-			    proof-trace-last-fontify-pos)))
+      (let ((fontifystart (proof-trace-fontify-pos)))
 	;; Catch errors here: this is to deal with ugly problem when
 	;; fontification of large output gives error Nesting too deep
-	;; for parser
+	;; for parser [see etc/isar/nesting-too-deep-for-parser.txt],
+	;; a serious flaw in XEmacs version of parse-partial-sexp
 	(unwind-protect
-	  (proof-fontify-region fontifystart (point))
+	    (proof-fontify-region fontifystart (point))
 	  (setq proof-trace-last-fontify-pos nil))
 	(set-buffer-modified-p nil)))))
 
+(defun proof-trace-buffer-finish ()
+  "Complete fontification in tracing buffer now that there's time to do so."
+  (let ((fontifystart (proof-trace-fontify-pos)))
+    (if fontifystart ;; may be done already
+	(save-excursion
+	   (set-buffer proof-trace-buffer)
+	   (proof-fontify-region fontifystart (point-max))))))
 
 
 
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 1f938ae7..f5706d74 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1020,6 +1020,9 @@ If NUM is negative, move upwards.  Return new span."
 (defun pg-goals-buffers-hint ()
   (pg-hint "Use \\[proof-display-some-buffers] to rotate output buffers; \\[pg-response-clear-displays] to clear response & trace."))
 
+(defun pg-slow-fontify-tracing-hint ()
+  (pg-hint "Large tracing output; decorating intermittently.  Use \\[pg-response-clear-displays] to clear trace."))
+
 (defun pg-response-buffers-hint (&optional nextbuf)
   (pg-hint
    (format
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index d1190b96..c171c1ca 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1176,6 +1176,9 @@ The return value is non-nil if the action list is now empty."
 		     ;; give a hint to the user in case we've finished
 		     ;; a batch of input
 		     (pg-processing-complete-hint)
+		     ;; complete the tracing buffer display in case 
+		     ;; we need to catch up.
+		     (pg-finish-tracing-display)
 		     ;; indicate finished
 		     t)
 	    ;; Otherwise, send the next command to the process.
@@ -1776,7 +1779,7 @@ Only works when system timer has microsecond count available."
 	  ;; quickly consecutive and large tracing outputs: go into slow mode
 	  (progn
 	    (setq pg-tracing-slow-mode t)
-	    (message "Fast tracing output: fontifying output intermittently")
+	    (pg-slow-fontify-tracing-hint)
 	    (setq pg-tracing-cleanup-timer
 		  (run-with-idle-timer 2 nil 'pg-finish-tracing-display))
 	    t)
@@ -1786,8 +1789,10 @@ Only works when system timer has microsecond count available."
 
 (defun pg-finish-tracing-display ()
   "Cancel tracing slow mode and ensure tracing buffer is fontified."
-  (setq pg-tracing-slow-mode nil)
-  (proof-trace-buffer-display ""))
+  (if pg-tracing-slow-mode
+      (progn
+	(setq pg-tracing-slow-mode nil)
+	(proof-trace-buffer-finish))))