aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2003-10-05 15:56:39 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2003-10-05 15:56:39 +0000
commit4936304bda8f1fed11aafd828be421eaf688a75d (patch)
tree9b59634b42cd9ef4fa5a4a6543696ef313b5f45c /CHANGES
parentd0e4aa049840658bc5ed900511f46e7d2d45619d (diff)
Updated.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES7
1 files changed, 5 insertions, 2 deletions
diff --git a/CHANGES b/CHANGES
index c32572b7..3028a9cb 100644
--- a/CHANGES
+++ b/CHANGES
@@ -137,8 +137,11 @@ 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.
+the identifier under the mouse, or the active region, as an argument.
+Bound globally to Control-Meta-Mouse-button1.
+
+Presently only configured in Isabelle/Isar, to parse terms (inside
+strings) and theorems (outside).
** GNU Emacs compatibility, simplified font-lock, handling nested comments