aboutsummaryrefslogtreecommitdiffhomepage
path: root/README.exper
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-12 08:33:46 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-12 08:33:46 +0000
commitd55abd121ba1a1c5ac49a52622d5e9cc526337aa (patch)
tree6ed7c7383f928de3394966f90c8e42570b424ae3 /README.exper
parent8c6b24410a2ef8d9767bfc1f4c12c0bfa6a0605c (diff)
Describe variable highlighting
Diffstat (limited to 'README.exper')
-rw-r--r--README.exper12
1 files 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.