aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2003-06-08 21:03:36 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2003-06-08 21:03:36 +0000
commit2bf1e7cf36499ceedd8b83fd97aa502623f4b622 (patch)
treeb3b9d87df67fd6ab04d7e0b6b7ce385cf74a67d4 /CHANGES
parenta4c179265640436c7c252fa3785a3c1d62e0953b (diff)
Updated.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES15
1 files changed, 15 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 470a305d..d32c6cdb 100644
--- a/CHANGES
+++ b/CHANGES
@@ -73,6 +73,15 @@ By default, the cursor jumps to the end of the locked region on an
error. Previously it also jumped on an interrupt. This is configurable
via `proof-shell-handle-error-or-interrupt-hook', which see.
+*** Automatic slow-down on fast tracing display
+
+Proof General will try to configure itself to update the display of
+tracing output infrequently when the prover is producing rapid,
+perhaps voluminous, output. This counteracts the situation that
+otherwise Emacs may consume more CPU than the proof assistant, trying
+to fontify and refresh the display as fast as output appears.
+See `proof-trace-output-slow-catchup' for setting.
+
*** Proof General -> Options menu changes
@@ -125,6 +134,12 @@ NB: Not yet enabled for Isabelle/Isar.
Electric terminator menu option more visible.
Reduce contrast for mouse highlighting of regions.
+*** Added `proof-shell-identifier-under-mouse-cmd'
+
+Allows PG to conveniently send a command to the prover which passes
+the identifier under the mouse as an argument. Bound globally to
+Control-Meta-Mouse-button1.
+
** GNU Emacs compatibility, simplified font-lock, handling nested comments