Add code to recognize fast tracing output from prover, and play slow catchup.

2 files changed, 114 insertions, 33 deletions

diff --git a/generic/pg-response.el b/generic/pg-response.el
index 001c154e..59840848 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -307,21 +307,30 @@ and start at the first error."
 ;; x-symbool and font-lock modes.  To fix that, though, we would have
 ;; to fix up the cut-and-paste behaviour somehow.
 
+(defvar proof-trace-last-fontify-pos nil)
+
 ;; An analogue of pg-response-display-with-face 
 (defun proof-trace-buffer-display (str)
-  "Display STR in the trace buffer."
-  (let (start)
-    (with-current-buffer proof-trace-buffer
-      (goto-char (point-max))
-      (newline)				
-      (setq start (point))
-      (insert str)
-      (unless (bolp) (newline))
-      ;; Catch errors here: this is to deal with ugly problem
-      ;; when fontification of large output gives 
-      ;; (error Nesting too deep for parser)
-      (condition-case nil
-	  (proof-fontify-region start (point)))
+  "Output STR in the trace buffer."
+  (with-current-buffer proof-trace-buffer
+    (goto-char (point-max))
+    (newline)
+    (or proof-trace-last-fontify-pos 
+	(setq proof-trace-last-fontify-pos (point)))
+    (insert 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)))
+	;; Catch errors here: this is to deal with ugly problem when
+	;; fontification of large output gives error Nesting too deep
+	;; for parser
+	(condition-case nil
+	  (proof-fontify-region fontifystart (point)))
+	(setq proof-trace-last-fontify-pos nil))
       (set-buffer-modified-p nil))))
 
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7589ead4..a4d51f54 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1171,6 +1171,30 @@ If none of these apply, display MESSAGE.
 MESSAGE should be a string annotated with 
 `proof-shell-eager-annotation-start', `proof-shell-eager-annotation-end'."
     (cond
+     ;; CASE tracing output: output in the tracing buffer instead
+     ;; of the response buffer
+     ((and proof-shell-trace-output-regexp
+	   (string-match proof-shell-trace-output-regexp message))
+      (proof-trace-buffer-display 
+       (if pg-use-specials-for-fontify
+	   message
+	 (pg-assoc-strip-subterm-markup message)))
+      (unless (and proof-trace-output-slow-catchup
+		   (pg-tracing-tight-loop))
+	(proof-display-and-keep-buffer proof-trace-buffer)
+	;; Force redisplay in case in a fast loop which keeps Emacs
+	;; fully-occupied processing prover output
+	;; FIXME: in case this is expensive, we should be adaptive
+	;; and redisplay only every so often.
+	(and (fboundp 'redisplay-frame)
+	     ;; XEmacs fn 
+	     (redisplay-frame)))
+      ;; If user quits during tracing output, send an interrupt
+      ;; to the prover.  Helps when Emacs is "choking".
+      (if (and quit-flag proof-action-list)
+	  (proof-interrupt-process)))
+
+       
      ;; CASE processing file: the prover is reading a file directly
      ;;
      ;; FIXME da: this interface is quite restrictive: might be
@@ -1321,26 +1345,6 @@ MESSAGE should be a string annotated with
 	       (split-string deps  
 			     proof-shell-theorem-dependency-list-split)))))
 
-     ;; CASE tracing output: output in the tracing buffer instead
-     ;; of the response buffer
-     ((and proof-shell-trace-output-regexp
-	   (string-match proof-shell-trace-output-regexp message))
-      (proof-trace-buffer-display 
-       (if pg-use-specials-for-fontify
-	   message
-	 (pg-assoc-strip-subterm-markup message)))
-      (proof-display-and-keep-buffer proof-trace-buffer)
-      ;; Force redisplay in case in a fast loop which keeps Emacs
-      ;; fully-occupied processing prover output
-      ;; FIXME: in case this is expensive, we should be adaptive
-      ;; and redisplay only every so often.
-      (and (fboundp 'redisplay-frame)
-	   ;; XEmacs fn 
-	   (redisplay-frame))
-      ;; If user quits during tracing output, send an interrupt
-      ;; to the prover.  Helps when Emacs is "choking".
-      (if (and quit-flag proof-action-list)
-	  (proof-interrupt-process)))
 	   
      (t
       ;; We're about to display a message.  Clear the response buffer
@@ -1360,6 +1364,8 @@ MESSAGE should be a string annotated with
 	   stripped)
 	 'proof-eager-annotation-face)))))
 
+
+
 (defun proof-shell-process-urgent-messages ()
   "Scan the shell buffer for urgent messages.
 Scanning starts from `proof-shell-urgent-message-scanner' and handles
@@ -1620,6 +1626,72 @@ by the filter is to send the next command from the queue."
 
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Tracing catch-up: prevent Emacs-consumes-all-CPU-fontifying phenomenon
+;;
+
+;; FIXME: not quite finished:
+;; -- need some way of coming out of tracing slow mode in case
+;;   tracing output has ended
+;; -- need to fontify remaining portion of buffer in case
+;;   tracing output has ended when in slow mode (and refresh
+;;   final display)  
+
+(defvar pg-last-tracing-output-time nil
+  "Time of last tracing output, as recorded by (current-time).")
+
+(defvar pg-tracing-slow-mode nil
+  "Non-nil for slow refresh mode for tracing output.")
+
+(defconst pg-slow-mode-duration 1
+  "Maximum duration of slow mode in seconds.")
+
+(defconst pg-fast-tracing-mode-threshold 50000
+  "Minimum microsecond delay between tracing outputs that triggers slow mode.")
+
+(defun pg-tracing-tight-loop ()
+  "Return non-nil in case it seems like prover is dumping a lot of output.
+This is a performance hack to avoid Emacs consuming CPU when prover is output
+tracing information.
+Only works when system timer has microsecond count available."
+  (let ((tm (current-time)))
+    (if pg-tracing-slow-mode
+	(if (eq (nth 0 pg-last-tracing-output-time) (nth 0 tm))
+	    ;; see if seconds has changed by at least pg-slow-mode-duration
+	    (if (> (- (nth 1 tm) (nth 1 pg-last-tracing-output-time)) 
+		   pg-slow-mode-duration)
+		;; go out of slow mode
+		(progn 
+		(setq pg-tracing-slow-mode nil)
+		(setq pg-last-tracing-output-time tm))
+	      ;; otherwise: stay in slow mode
+	      t)
+	  ;; different seconds-major count: go out of slow mode
+	  (progn 
+	    (setq pg-last-tracing-output-time tm)
+	    (setq pg-tracing-slow-mode nil)))
+      ;; ordinary mode: examine difference since last output
+      (if
+	  (and pg-last-tracing-output-time 
+	       (eq (nth 0 tm) (nth 0 pg-last-tracing-output-time))
+	       (eq (nth 1 tm) (nth 1 pg-last-tracing-output-time))
+	       ;; Same second: examine microsecond
+	       (> (nth 2 tm) 0) ;; some systems always have zero count
+	       ;; 
+	       (< (- (nth 2 tm) (nth 2 pg-last-tracing-output-time)) 
+		  pg-fast-tracing-mode-threshold))
+	  ;; quickly consecutive tracing outputs: go into slow mode
+	  (progn
+	    (setq pg-tracing-slow-mode t)
+	    (message "Fast tracing output: playing slow catch-up")
+	    t)
+	;; not quick enough to trigger slow mode: allow screen update
+	(setq pg-last-tracing-output-time tm)
+	nil))))
+	    
+
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;