diff options
| author | David Aspinall | 2002-07-18 09:56:25 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-07-18 09:56:25 +0000 |
| commit | a44df3c847cf3d8056d7ccf3dc38d5afbd0e86e7 (patch) | |
| tree | 97bfe5242a0758dd3b670fb269b78e3c7b527024 | |
| parent | a063632054162073ddb0aca986c366094d569e05 (diff) | |
Mention experimental nature
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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. |
