-*- outline -*-  

* Main Changes for Proof General 4.0 from 3.7.X

** Generic changes

*** XEmacs is no longer supported; PG only works with GNU Emacs 22.2+

*** Font-lock based Unicode Tokens mode replaces X-Symbol

*** Document-centred mechanisms added:
    - output retained for script buffer popups
    - background colouring for locked region can be disabled
    - auto raise of prover output buffers can be disabled
    Depending on input language and interaction output, this
    may enable a "document centred" way of working, when output
    buffers can be ignored and hidden. 
    Use full annotation to keep output when several steps are taken.

*** New user configuration options
    proof-auto-raise-buffers  (set to nil for manual control)
    proof-full-decoration     (add full decoration to input)

*** Removed user configuration options
    proof-toolbar-use-button-enablers  (now always used)

*** Altered prover configuration settings
    pg-insert-output-as-comment-fn:  removed
    proof-shell-strip-output-markup: required for cut-and-paste
    proof-electric-terminator-noterminator: allows non-insert of terminator


** Isabelle/Isar changes

*** Electric terminator works without inserting terminator

*** Line numbers reported during script management

*** Sync problems with bad input prevented by command wrapping

*** Isabelle Settings now organised in sub-menus


** Coq changes

*** Holes mode can be turned on/off