1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
Experimental features in this release of Proof General.
======================================================
Proof General includes a few features designated as "experimental"
because they have not been fully tested or completed. Enabling these
will usually have no detrimental effects on using standard features of
PG, but the experimental features themselves may be less robust.
Experimental features can be enabled by customizing the variable
`proof-experimental-features'. If you set this to `nil', and restart
Proof General, then the features mentioned below will be disabled.
We encourage users to work with this flag set and test the features,
but being aware that the features are regarded as incomplete (problem
reports and suggestions for improvements are welcomed).
Current "experimental" features
===============================
** "Move up" and "Move down" functions in context span menu
(use right-click on highlighted spans), also bound on
C-M-up/C-M-down.
** Theorem dependencies: displaying and highlighting dependencies.
Dependencies (e.g. lemmas) for a theorem are highlighted in
yellow, places where the theorem is used are highlighted
in orange. This allows easy editing of theories to remove
dead lemmas, re-order proofs, etc.
This only works in Isabelle at the moment. (Support is required
from other proof assistant authors: please suggest to them!). You
must select the Isabelle setting "Theorem Dependencies" before
starting Isabelle, to enable gathering of data.
** 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, often, but it depends on the context and may be
wrong. In Isabelle/classic the type information is useless.
This feature is a vague 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 for Proof General to send
back to the prover, so only variables bound at the outer level can
have sensible information displayed, via the "term" command.
Known problems with experimental features
=========================================
** Move up/down functions may spoil visibility behaviour.
|
