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
|
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 `t', and restart
Proof General, then the features mentioned below will be enabled.
We encourage users to set this flag 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.
Only works for Isabelle/classic at the moment (support is
required from proof assistant authors: please mention to them).
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.
Known problems with experimental features
=========================================
** Move up/down functions make spoil visibility behaviour.
|
