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.

0 files changed, 0 insertions, 0 deletions