| Age | Commit message (Collapse) | Author |
|---|
|
up-to-date.
|
|
|
|
columns mode).
|
|
enabling it disables electric-terminator and vice-versa. In case both
are non nil at the same time, then electric teminator has priority. If
people like it we may propose this to other modes than coq.
+ fixed window layout policy.
|
|
|
|
'horizontal 'vertical 'smart policy.
|
|
|
|
|
|
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.
|
|
|
|
clone-buffer to work, at least superficially.
|
|
the wrong place).
|
|
is too small. However if the frame is too small the bug remains (but
it is much less probable).
|
|
|
|
|
|
|
|
|
|
not available
|
|
|
|
|
|
|
|
|
|
|
|
cleanups
|
|
|
|
|
|
|
|
cursor.
|
|
|
|
|
|
|
|
font-lock-append-text-property [no behaviour change]
|
|
namespaces fixes.
pre-shell-start-hook: remove this, use default names for modes
proof-compat: simplify architecture flags, use standard (featurep 'xemacs).
|
|
output.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
setting.
|
|
|
|
|
|
|
|
frames only to delete them.
|
|
|
|
|
|
compatibility.
|
