-*- outline -*-  

* Main Changes for Proof General 4.0 from 3.7.1

** Generic changes

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

*** Font-lock based Unicode Tokens mode replaces X-Symbol
    Unicode Tokens has been significantly improved since PG 3.7.1,
    and now works purely at a "presentation" level without changing 
    buffer contents.  For best results, Emacs 23 is recommended.

*** Document-centred mechanisms added:
    - auto raise of prover output buffers can be disabled
    - output retained for script buffer popups
    - background colouring for locked region can be disabled
    - ...but "sticky" colouring for errors can be used
    - edit on processed region can automatically undo

    Depending on input language and interaction output, this may
    enable a useful "document centred" way of working, when output
    buffers can be ignored and hidden.
    Use "full annotation" to keep output when several steps are taken.

*** Improved prevention of Undo in locked region
    proof-allow-undo-in-read-only: now defaults to nil

*** Simplified version of comint now used for proof shell
    To improve efficiency, a cut-down version of comint is now used.
    Editing, history and decoration in the shell (*coq*, *isabelle*,
    etc) are impoverished compared with PG 3.X.

*** Proof General -> Options menu extended and rearranged
    - new menu for useful minor modes suggests modes that PG supports

*** New user configuration options (also on Proof General -> Options)
    proof-colour-locked       (use background colour for checked text)
    proof-auto-raise-buffers  (set to nil for manual window control)
    proof-full-decoration     (add full decoration to input text)
    proof-sticky-errors       (add highlighting for commands that caused error)
    proof-shell-quiet-errors  (non-nil to disable beep on error; default=nil)
    proof-minibuffer-messages (non-nil to show prover messages; default=nil)

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

*** Altered prover configuration settings (internal)

    urgent message matching is now anchored; configurations for
    `proof-shell-clear-response-regexp', etc, must match
    strings which begin with `proof-shell-eager-annotation-start'.

    proof-shell-strip-output-markup: added for cut-and-paste
    proof-electric-terminator-noterminator: allows non-insert of terminator

    pg-insert-output-as-comment-fn: removed (use p-s-last-output)
    proof-shell-wakeup-char: removed (special chars deprecated)
    pg-use-specials-for-fontify: removed (ditto)
    proof-shell-prompt-pattern: removed (was only for shell UI)
    proof-shell-abort-goal-regexp: removed (ordinary response)
    proof-shell-error-or-interrupt-seen: removed, use p-s-last-output-kind
    proof-script-next-entity-regexps,next-entity-fn: removed (func-menu dead)

*** Primary distribution formats changed
    The RPM and zip file formats have been removed.
    We are very grateful to third-party packagers for Debian and Fedora
    for distributing packaged versions of PG.

** Isabelle/Isar changes

*** Support undo back into completed proofs (linear_undo).

*** 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

*** Only supports Coq 8.1, support for earlier versions dropped.

*** Holes mode can be turned on/off and has its own minor mode