Tweak message and display model, in particular, make sure that when a

response appears above a goals output, the goals output is displayed
second, so it is the one that remains visible to the user in the
default 2-pane mode.  This works with output like this in HOL Light:

  Warning: Free variables in goal: A, B
  val it : goalstack = 1 subgoal (1 total)
  ...

and similar cases in Isabelle and Coq.

The fix involves some ugly messing with the flags for clearing the
response buffer (see `pg-response-maybe-erase').  This could surely be
streamlined.

3 files changed, 68 insertions, 41 deletions

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 55a64bfc..ecb5ce74 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -73,23 +73,25 @@ May enable proof-by-pointing or similar features.
 ;;
 ;; Goals buffer processing
 ;;
-(defun pg-goals-display (string)
+(defun pg-goals-display (string keepresponse)
   "Display STRING in the `proof-goals-buffer', properly marked up.
-Converts term substructure markup into mouse-highlighted extents."
+Converts term substructure markup into mouse-highlighted extents.
+
+The response buffer may be cleared to avoid confusing the user
+with output associated with a previous goals message.  This
+function tries to do that by calling `pg-response-maybe-erase'.
+
+If KEEPRESPONSE is non-nil, we assume that a response message
+corresponding to this goals message has already been displayed
+before this goals message (see `proof-shell-handle-delayed-output'),  
+so the response buffer should not be cleared."
   (save-excursion
     ;; Response buffer may be out of date. It may contain (error)
     ;; messages relating to earlier proof states
 
-    ;; NB: this isn't always the case.  In Isabelle
-    ;; we get <WARNING MESSAGE> <CURRENT GOALS> output,
-    ;; or <WARNING MESSAGE> <ORDINARY MESSAGE>.  Both times
-    ;; <WARNING MESSAGE> would be relevant.
-    ;; We should only clear the output that was displayed from
-    ;; the *previous* prompt.
-
     ;; Erase the response buffer if need be, maybe removing the
     ;; window.  Indicate it should be erased before the next output.
-    (pg-response-maybe-erase t t)
+    (pg-response-maybe-erase t t nil keepresponse)
 
     ;; Erase the goals buffer and add in the new string
     (set-buffer proof-goals-buffer)
diff --git a/generic/pg-response.el b/generic/pg-response.el
index a24376b8..6ee58713 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -219,14 +219,27 @@ For multiple frame mode, this function obeys the setting of
 
 ;;;###autoload
 (defun pg-response-maybe-erase
-  (&optional erase-next-time clean-windows force)
-  "Erase the response buffer according to `pg-response-erase-flag'.
+  (&optional erase-next-time clean-windows force keep)
+  "Erase the response buffer, according to confusing flag combinations.
+
+Mainly, we look at `pg-response-erase-flag' and clear the
+response buffer if this is non-nil, but NOT the special
+symbol 'invisible.
+
 ERASE-NEXT-TIME is the new value for the flag.
-If CLEAN-WINDOWS is set, use `proof-clean-buffer' to do the erasing.
-If FORCE, override `pg-response-erase-flag'.
 
-If the user option `proof-tidy-response' is nil, then
-the buffer is only cleared when FORCE is set.
+FORCE overrides the flag to force cleaning.
+
+KEEP overrides the flag to prevent cleaning.
+
+FORCE takes precedent over KEEP.
+
+If CLEAN-WINDOWS is set, use `proof-clean-buffer' to do the erasing,
+otherwise we use `bufhist-checkpoint-and-erase' to record an
+undo history entry for the current buffer contents.
+
+If the user option `proof-tidy-response' is nil, the buffer
+will never be cleared unless FORCE is set.
 
 No effect if there is no response buffer currently.
 Returns non-nil if response buffer was cleared."
@@ -234,6 +247,7 @@ Returns non-nil if response buffer was cleared."
     (let ((inhibit-read-only t)
 	  (doit (or (and
 		     proof-tidy-response
+		     (not keep)
 		     (not (eq pg-response-erase-flag 'invisible))
 		     pg-response-erase-flag)
 		    force)))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 9cdce998..c889b789 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1472,43 +1472,49 @@ by the filter is to send the next command from the queue."
     (pg-response-display str)))
 
 (defun proof-shell-handle-delayed-output ()
-  "Display delayed outputs, when queue is stopped or completed.
+  "Display delayed goals/responses, when queue is stopped or completed.
 This function handles the cases of `proof-shell-output-kind' which
 are not dealt with eagerly during script processing, namely
 'response and 'goals types.
 
-This is useful even with empty delayed output as it can
-clear the buffers.
+This is useful even with empty delayed output as it will empty
+the buffers.
 
 The delayed output is in the region
 \[proof-shell-delayed-output-start,proof-shell-delayed-output-end].
 
+If no goals classified output is found, the whole output is
+displayed in the response buffer.
+
 If goals output is found, the last matching instance, possibly
-bounded by `proof-shell-end-goals-regexp', will be displayed.
-Any output that appears *before* the first goals output (but
+bounded by `proof-shell-end-goals-regexp', will be displayed
+in the goals buffer (and may be further analysed by Proof General).
+
+Any output that appears *before* the last goals output (but
 after messages classified as urgent, see `proof-shell-filter')
-will also be displayed in the response buffer.  For example,
-if OUTPUT has this form:
+will also be displayed in the response buffer.
+
+For example, if OUTPUT has this form:
 
   MESSSAGE-1
   GOALS-1
   MESSAGE-2
   GOALS-2
+  JUNK
 
 then GOALS-2 will be displayed in the goals buffer, and MESSAGE-2
-in the response buffer.  Notice that the above alternation can
+in the response buffer.  JUNK will be ignored.
+
+Notice that the above alternation (and separation of JUNK) can
 only be distinguished if both `proof-shell-start-goals-regexp'
-and `proof-shell-end-goals-regexp' are set.  With just the
-former, MESSAGE-1 GOALS-1 MESSAGE-2 would all appear in
-the response buffer.
+and `proof-shell-end-goals-regexp' are set.  With just the start
+goals regexp set, GOALS-2 JUNK will appear in the goals buffer
+and no response output would occur.
    
 The goals and response outputs are copied into
 `proof-shell-last-goals-output' and
 `proof-shell-last-response-output' respectively.
 
-If no other kind of classified output is found, the default
-is to display the output in the response buffer.
-
 The value returned is the value for `proof-shell-last-output-kind',
 i.e., 'goals or 'response."
   (let ((start proof-shell-delayed-output-start)
@@ -1522,8 +1528,9 @@ i.e., 'goals or 'response."
 	    (gstart (or (match-end 1)    ; start of actual display
 			gmark))
 	    (rstart start)		 ; possible response before goals
-	    (gend   end))
-       ;; Find the last goal string in the output
+	    (gend   end)
+	    both)			 ; flag for response+goals
+
        (goto-char gstart)
        (while (re-search-forward proof-shell-start-goals-regexp end t)
 	 (setq gmark (match-beginning 0))
@@ -1537,19 +1544,23 @@ i.e., 'goals or 'response."
 		 end)))
        (setq proof-shell-last-goals-output
 	     (buffer-substring-no-properties gstart gend))
+
+       ;; FIXME heuristic: 4 allows for annotation in end-goals-regexp [is it needed?]
+       (setq both
+	     (> (- gmark rstart) 4))
+       (if both
+	   (proof-shell-display-output-as-response 
+	    flags
+	    (buffer-substring-no-properties rstart gmark)))
+       ;; display goals output second so it persists in 2-pane mode
        (unless (memq 'no-goals-display flags)
-	 (pg-goals-display proof-shell-last-goals-output))
-       ;; also allow (for Coq) any preceding output as a response
-       ;; FIXME heuristic: 4 allows for annotation in end-goals-regexp
-       (when (> (- gmark rstart) 4)
-	 (proof-shell-display-output-as-response
-	  flags
-	  (buffer-substring-no-properties rstart gmark)))
-       ;; primary output kind is goals
+	 (pg-goals-display proof-shell-last-goals-output both))
+       ;; indicate a goals output has been given
        'goals))
 
-   (t ; Any unclassified output will appear as a response.
+   (t
     (proof-shell-display-output-as-response flags proof-shell-last-output)
+    ;; indicate that (only) a response output has been given
     'response))
   
   (run-hooks 'proof-shell-handle-delayed-output-hook)))