aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CHANGES11
1 files changed, 10 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 627d4bf3..124da18b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,13 +45,22 @@ For minor issues, see isa/BUGS.
** Isabelle Changes
-Isabelle/Isar syntax changes, other tweaks for Isabelle2002.
+*** Isabelle/Isar syntax changes, other tweaks for Isabelle2002.
+
Switch to using Isabelle/Isar by default for .thy files.
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
+
+Variables are made active in the goals buffer. Hovering the mouse
+over an identifier shows its type. [IN PROGRESS; faulty with X-Sym]
+
+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.
+
** Coq Changes