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.

1 files changed, 20 insertions, 6 deletions

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)))