Unhappily added proof-shell-leave-annotations-in-output hack.

3 files changed, 103 insertions, 50 deletions

diff --git a/CHANGES b/CHANGES
index 81ebe3d5..e5938e86 100644
--- a/CHANGES
+++ b/CHANGES
@@ -65,5 +65,16 @@ Only in the developers' release
 Internal changes for developers to note
 ---------------------------------------
 
+* proof-shell-leave-annotations-in-output variable has been added.
+  This allows quick and dirty mark up of output from the proof
+  assistant using special characters with codes above 128 and
+  font-lock.  Such characters are hidden from display in the
+  output buffers.  
+  However, it is NOT recommended to use this mechanism, because
+  it breaks the usability of cut and paste (which copies the
+  special characters).  Furthermore the entire mechanism of
+  using special character codes is fragile and needs replacing
+  in future versions of Proof General!
+
 * Code cleanups and improvements.
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 2da756cf..aab2e4d6 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -113,14 +113,16 @@ use because of a bug."
 (defcustom proof-strict-read-only 
   ;; For FSF Emacs, strict read only is buggy when used in
   ;; conjunction with font-lock.
-
   ;; The second conjunctive ensures that the expression is either
-  ;; `nil' or `strict' (and not 15).  
+  ;; `nil' or `strict' (and not 15!!).  
   (and (string-match "XEmacs" emacs-version) 'strict)
   "*Whether Proof General is strict about the read-only region in buffers.
 If non-nil, an error is given when an attempt is made to edit the
 read-only region.  If nil, Proof General is more relaxed (but may give
-you a reprimand!)
+you a reprimand!).
+
+If you change proof-strict-read-only during a session, you must use
+\"Restart\" (proof-shell-restart)
 
 The default value for proof-strict-read-only depends on which
 version of Emacs you are using.  In FSF Emacs, strict read only is buggy
@@ -130,13 +132,12 @@ when it used in conjunction with font-lock, so it is disabled by default."
 
 (defcustom proof-auto-retract
   nil
-  ;; Not implemented yet, only an idea.
   "*If non-nil, retract automatically when locked region is edited.
 With this option active, the locked region will automatically be
 unlocked when the user attempts to edit it.   To make use of this
 option, proof-strict-read-only should be turned off.
 
-Note: this feature has not been implemented yet."
+Note: this feature has not been implemented yet, it's only an idea."
   :type 'boolean
   :group 'proof-general)
 
@@ -157,7 +158,6 @@ This option is not fully-functional at the moment."
   :type 'boolean
   :group 'proof-general)
 
-
 (defcustom proof-script-command-separator " "
   "*String separating commands in proof scripts.
 For example, if a proof assistant prefers one command per line, then 
@@ -956,6 +956,14 @@ data triggered by `proof-shell-retract-files-regexp'."
   :type '(choice function (const nil))
   :group 'proof-shell)
 
+(defcustom proof-shell-leave-annotations-in-output nil
+  "Flag indicating whether to strip annotations from output or not.
+\"annotations\" are special characters with the top bit set.
+If annotations are left in, they are made invisible and can be used
+to do syntax highlighting with font-lock."
+  :type 'boolean
+  :group 'proof-shell)
+
 
 
 ;;
@@ -995,7 +1003,7 @@ variables."
 
 (defcustom proof-shell-handle-delayed-output-hook
   '(proof-pbp-focus-on-first-goal)
-  "Hooks run after new output has been displayed in the response buffer."
+  "Hooks run after new output has been displayed in goals or response buffer."
   :type '(repeat function)
   :group 'proof-shell)
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 022f592f..141a61d6 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -587,11 +587,12 @@ If FORCE, override proof-shell-erase-response-flag."
 (defvar proof-shell-delayed-output nil
   "Last interesting output from proof process output and what to do with it.
 
-This is a list of tuples of the form (type . string). type is either
+This is a list of tuples of the form (TYPE . STRING). type is either
 'analyse or 'insert. 
 
 'analyse denotes that string's term structure  ought to be analysed
          and displayed in the `proof-goals-buffer'
+
 'insert  denotes that string ought to be displayed in the
          `proof-response-buffer' ")
 
@@ -604,13 +605,15 @@ This is a list of tuples of the form (type . string). type is either
 	   (out (make-string l ?x)) 
 	   c span)
 
-      ;; Form output string by removing characters 
-      ;; 128 or greater.
-      (while (< ip l)	
-	(if (< (setq c (aref string ip)) 128)
-	    (progn (aset out op c)
-		   (incf op)))
-	(incf ip))
+      ;; Form output string by removing characters 128 or greater,
+      ;; (ALL annotations), unless proof-shell-leave-annotations-in-output 
+      ;; is set.
+      (unless proof-shell-leave-annotations-in-output
+	(while (< ip l)	
+	  (if (< (setq c (aref string ip)) 128)
+	      (progn (aset out op c)
+		     (incf op)))
+	  (incf ip)))
 
       ;; Response buffer may be out of date. It may contain (error)
       ;; messages relating to earlier proof states
@@ -636,7 +639,12 @@ This is a list of tuples of the form (type . string). type is either
       ;; of end.  Might be nicer to keep it at "current" subgoal
       ;; a la Isamode, but never mind.
       (erase-buffer)
-      (insert (substring out 0 op))
+
+      ;; Insert the (possibly cleaned up) string.
+      (if proof-shell-leave-annotations-in-output
+	  (insert string)
+	(insert (substring out 0 op)))
+
       (proof-x-symbol-decode-region (point-min) (point-max))
       (proof-display-and-keep-buffer proof-goals-buffer (point-min))
 
@@ -692,9 +700,9 @@ This is a list of tuples of the form (type . string). type is either
 		     topl (cdr topl))
 	  (pbp-make-top-span ip (car topl)))))))
 
-(defun proof-shell-strip-annotations (string)
+(defun proof-shell-strip-special-annotations (string)
   "Strip special annotations from a string, returning cleaned up string.
-Special annotations are characters with codes higher than
+*Special* annotations are characters with codes higher than
 'proof-shell-first-special-char'."
   (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x )))
     (while (< ip l)
@@ -721,8 +729,10 @@ Returns the string (with faces) in the specified region."
       (setq start (search-backward-regexp start-regexp))
       (setq end (- (search-forward-regexp end-regexp)
 				   (length (match-string 0))))
-      (setq string
-	    (proof-shell-strip-annotations (buffer-substring start end))))
+      (unless proof-shell-leave-annotations-in-output
+	(setq string
+	      (proof-shell-strip-special-annotations 
+	       (buffer-substring start end)))))
     ;; Erase if need be, and erase next time round too.
     (proof-shell-maybe-erase-response t nil)
     (proof-response-buffer-display string append-face)))
@@ -730,31 +740,48 @@ Returns the string (with faces) in the specified region."
 (defun proof-shell-handle-delayed-output ()
   "Display delayed output.
 This function expects 'proof-shell-delayed-output' to be a cons cell
-of the form '(insert . txt) or '(analyse . txt).
+of the form ('insert . TXT) or ('analyse . TXT).
 See the documentation for `proof-shell-delayed-output' for further details."
   (let ((ins (car proof-shell-delayed-output))
 	(str (cdr proof-shell-delayed-output)))
     (cond 
+     ;; 
+     ;; 1. Text to be inserted in response buffer.
+     ;;
      ((eq ins 'insert)
-       ; (unless (string-equal str "done") ;; FIXME da: nasty, breaks something?
-	(setq str (proof-shell-strip-annotations str))
-	(with-current-buffer proof-response-buffer
-	  ;; FIXME da: have removed this, possibly it junks 
-	  ;; relevant messages.  Instead set a flag to indicate
-	  ;; that response buffer should be cleared before the
-	  ;; next command.
-	  ;; (erase-buffer)
-
-	  ;; NEW!
-	  ;; Erase the response buffer if need be, and indicate that
-	  ;; it is to be erased again before the next message.
-	  (proof-shell-maybe-erase-response t nil)
-	  (let ((pos (point)))
-	    (insert str)
-	    (proof-x-symbol-decode-region pos (point)))
-	  (proof-display-and-keep-buffer proof-response-buffer)))
+      ;; FIXME da: this next line is nasty, it breaks something?
+      ;;   (unless (string-equal str "done")  
+      ;; Think this was meant as a get out clause from somewhere.
+      ;; Maybe if the output string from the prover is empty?
+      ;; Anyway, we leave it alone now, maybe to see some spurious 
+      ;; "done" displays 
+
+      (unless proof-shell-leave-annotations-in-output
+	(setq str (proof-shell-strip-special-annotations str)))
+
+      (with-current-buffer proof-response-buffer
+	;; FIXME da: have removed this, possibly it junks 
+	;; relevant messages.  Instead set a flag to indicate
+	;; that response buffer should be cleared before the
+	;; next command.
+	;; (erase-buffer)
+
+	;; NEW!
+	;; Erase the response buffer if need be, and indicate that
+	;; it is to be erased again before the next message.
+	(proof-shell-maybe-erase-response t nil)
+	(let ((pos (point)))
+	  (insert str)
+	  (proof-x-symbol-decode-region pos (point)))
+	(proof-display-and-keep-buffer proof-response-buffer)))
+     ;;
+     ;; 2. Text to be inserted in goals buffer
+     ;;
      ((eq ins 'analyse)
       (proof-shell-analyse-structure str))
+     ;;
+     ;; 3. Nothing else should happen
+     ;;
      (t (assert nil))))
   (run-hooks 'proof-shell-handle-delayed-output-hook)
   (setq proof-shell-delayed-output (cons 'insert "done")))
@@ -796,7 +823,7 @@ Then we call `proof-shell-handle-error-hook'. "
       (save-excursion ;current-buffer
 	(set-buffer proof-goals-buffer)
 	(erase-buffer)
-	(insert (proof-shell-strip-annotations 
+	(insert (proof-shell-strip-special-annotations 
 		   (cdr proof-shell-delayed-output)))
 	(proof-display-and-keep-buffer proof-goals-buffer)))
 
@@ -893,7 +920,7 @@ assistant."
     'interrupt)
 
    ((proof-shell-string-match-safe proof-shell-error-regexp string)
-    (cons 'error (proof-shell-strip-annotations
+    (cons 'error (proof-shell-strip-special-annotations
 		  (substring string
 			     (match-beginning 0)))))
 
@@ -1268,7 +1295,7 @@ strings between eager-annotation-start and eager-annotation-end."
 	(if (setq end
 		  (re-search-forward proof-shell-eager-annotation-end nil t))
 	    (proof-shell-process-urgent-message
-	     (proof-shell-strip-annotations (buffer-substring start end))))
+	     (proof-shell-strip-special-annotations (buffer-substring start end))))
 	;; Set the marker to the end of the last message found, if any.
 	;; Must take care to keep the marger behind the process marker
 	;; otherwise no output is seen!  (insert-before-markers in comint)
@@ -1425,20 +1452,19 @@ output."
 	      (proof-shell-handle-delayed-output)))))))
 
 
-(defun proof-shell-dont-show-annotations ()
-  "Set display values of annotations in process buffer to be invisible.
+(defun proof-shell-dont-show-annotations (&optional buffer)
+  "Set display values of annotations in BUFFER to be invisible.
 
 Annotations are characters 128-255."
   (save-excursion
-    (set-buffer proof-shell-buffer)
+    (set-buffer (or buffer (current-buffer)))
     (let ((disp (make-display-table))
 	  (i 128))
       (while (< i 256)
 	(aset disp i [])
 	(incf i))
       (cond ((fboundp 'add-spec-to-specifier)
-	     (add-spec-to-specifier current-display-table disp
-				    proof-shell-buffer))
+	     (add-spec-to-specifier current-display-table disp (current-buffer)))
 	    ((boundp 'buffer-display-table)
 	     (setq buffer-display-table disp))))))
 
@@ -1529,11 +1555,16 @@ before and after sending the command."
 
   ;; FIXME da: before entering proof assistant specific code,
   ;; we'd do well to check that process is actually up and
+    ;; Should already be in proof-goals-buffer, really.
   ;; running now.  If not, call the process sentinel function
   ;; to display the buffer, and give an error.
   ;; (Problem to fix is that process can die before sentinel is set:
   ;;  it ought to be set just here, perhaps: but setting hook here
   ;;  had no effect for some odd reason).
+
+  ;; da added this 23/8/99.  LEGO set font-lock-terms in shell,
+  ;; but didn't use it until now.
+  (proof-font-lock-minor-mode)
   ))
 
 ;; watch difference with proof-shell-menu, proof-shell-mode-menu.
@@ -1549,7 +1580,6 @@ before and after sending the command."
 
 (defun proof-font-lock-minor-mode ()
   "Start font-lock as a minor mode in the current buffer."
-
   ;; setting font-lock-defaults explicitly is required by FSF Emacs
   ;; 20.2's version of font-lock
   (make-local-variable 'font-lock-defaults)
@@ -1560,14 +1590,18 @@ before and after sending the command."
   "Initialise the goals buffer after the child has been configured."
   (save-excursion
     (set-buffer proof-goals-buffer)
-    (proof-font-lock-minor-mode)))
-
+    (proof-font-lock-minor-mode)
+    ;; Turn off the display of annotations here
+    (proof-shell-dont-show-annotations)))
 
 (defun proof-response-config-done ()
   "Initialise the response buffer after the child has been configured."
   (save-excursion
     (set-buffer proof-response-buffer)
-    (proof-font-lock-minor-mode)))
+    (proof-font-lock-minor-mode)
+    ;; Turn off the display of annotations here
+    (proof-shell-dont-show-annotations)))
+
 
 (defun proof-shell-config-done ()
   "Initialise the specific prover after the child has been configured."