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.