From d55abd121ba1a1c5ac49a52622d5e9cc526337aa Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 12 Aug 2002 08:33:46 +0000
Subject: Describe variable highlighting

---
 README.exper | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/README.exper b/README.exper
index 494ae0d8..79ef743d 100644
--- a/README.exper
+++ b/README.exper
@@ -33,6 +33,12 @@ Current "experimental" features
    You must select the Isabelle option "Theorem Dependencies",
    and then restart Isabelle.
 
-
-
-
+** Active highlighting for variables in Isabelle.
+   Moving the mouse over variables in the goal display will display
+   some information.  The information in Isabelle/Isar is the type of
+   the variable, usually.  In Isabelle it is useless.
+   This feature is a hint of what could be done with proper subterm
+   markup from the Isabelle engine.  Without this, it cannot work
+   well, because no context is available to Proof General, so only
+   variables bound at the outer level can have meaningful information
+   displayed, via the "term" command.
-- 
cgit v1.2.3