| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
Martin-Dorel)
|
|
clone-buffer to work, at least superficially.
|
|
|
|
|
|
|
|
cleanups
|
|
|
|
|
|
cursor.
|
|
ordinary span construction.
|
|
|
|
namespaces fixes.
pre-shell-start-hook: remove this, use default names for modes
proof-compat: simplify architecture flags, use standard (featurep 'xemacs).
|
|
output.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
display.
|
|
|
