Dont return a fontified string in proof-response-buffer-display.

2 files changed, 15 insertions, 6 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 60bcd2d7..4f2b1678 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -227,6 +227,9 @@ Does nothing if proof assistant is already running."
       (save-excursion
 	(set-buffer proof-shell-buffer)
 	
+	;; PG 3.4: clear output from previous sessions.
+	(erase-buffer)
+
 	;; FIXME: Disable 16 Bit
 	;; We noticed that for LEGO, it otherwise converts annotations
 	;; to characters with (non-ASCII) code around 3000 which screws
@@ -255,6 +258,9 @@ Does nothing if proof assistant is already running."
 	      (and (fboundp 'toggle-enable-multibyte-characters)
 		   (toggle-enable-multibyte-characters -1))
 	      (funcall proof-mode-for-goals))
+	  ;; 
+	  ;; If the process died, switch to the buffer to
+	  ;; display the error messages to the user.
 	  (switch-to-buffer proof-shell-buffer)
 	  (error "%s process exited!" proc)))
       (message "Starting %s process... done." proc))))
@@ -763,8 +769,9 @@ last match in the buffer for END-REGEXP.  The match for END-REGEXP
 is not part of the specified region.  This mechanism means if there
 are multiple matches for START-REGEXP and END-REGEXP, we match the
 largest region containing them all.
-This is a subroutine of proof-shell-handle-error.
-Returns the string (with faces) in the specified region."
+This is a subroutine of proof-shell-handle-error."
+;; 3.4: doesn't return the string any more.
+;; Returns the string (with faces) in the specified region."
   (let (start end string)
     (save-excursion
       (set-buffer proof-shell-buffer)
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 39f139f6..eea38ce0 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -317,8 +317,7 @@ Fontifies according to the buffer's font lock defaults.
 Uses proof-x-symbol-decode to decode tokens if x-symbol is present.
 
 If proof-shell-leave-annotations-in-output is set, remove characters
-with top bit set after fontifying so they can be used for
-fontification.
+with top bit set after fontifying so they don't spoil cut and paste.
 
 Returns new END value."
   ;; We fontify first because decoding changes char positions.
@@ -392,7 +391,8 @@ Returns new END value."
 ;; FIXME: this function should be combined with
 ;; proof-shell-maybe-erase-response-buffer. 
 (defun proof-response-buffer-display (str &optional face)
-  "Display STR with FACE in response buffer and return fontified STR."
+  "Display STR with FACE in response buffer."
+  ;; 3.4: no longer return fontified STR, it wasn't used.
   (if (string-equal str "\n")	
       str				; quick exit, no display.
   (let (start end)
@@ -414,7 +414,9 @@ Returns new END value."
 	  (font-lock-append-text-property start end 'face face))
       ;; This returns the decorated string, but it doesn't appear 
       ;; decorated in the minibuffer, unfortunately.
-      (buffer-substring start (point-max))))))
+      ;; 3.4: remove this for efficiency.
+      ;; (buffer-substring start (point-max))
+      ))))
 
 (defun proof-display-and-keep-buffer (buffer &optional pos)
   "Display BUFFER and mark window according to `proof-dont-switch-windows'.