aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-07-18 09:56:25 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-07-18 09:56:25 +0000
commita44df3c847cf3d8056d7ccf3dc38d5afbd0e86e7 (patch)
tree97bfe5242a0758dd3b670fb269b78e3c7b527024 /CHANGES
parenta063632054162073ddb0aca986c366094d569e05 (diff)
Mention experimental nature
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES4
1 files changed, 2 insertions, 2 deletions
diff --git a/CHANGES b/CHANGES
index 1bf45a3b..1e5cfb69 100644
--- a/CHANGES
+++ b/CHANGES
@@ -55,10 +55,10 @@ Support next error function.
Isabelle classic mode: highlighting tweaks for ML code contributed by
Lucas Dixon (lucasd@dai.ed.ac.uk)
-*** Active highlighting of variables
+*** Active highlighting of variables [ EXPERIMENTAL FEATURE: has issues ]
Variables are made active in the goals buffer. Hovering the mouse
-over an identifier shows its type. [IN PROGRESS; faulty with X-Sym]
+over an identifier shows its type.
This handy feature is a glimpse of what could be done with proper
subterm markup, which needs support to be added in the Isabelle core.