diff options
| author | David Aspinall | 2009-08-07 14:43:06 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-08-07 14:43:06 +0000 |
| commit | b1ba6ba04341ba43b2650ce0e45c7fd15111c529 (patch) | |
| tree | 4b3756b9494c03ce6b2b3276f4f1171e8069e3f8 | |
| parent | 7b0b49cdc9fa9883b1fcd246608b7dc5fac7b5b2 (diff) | |
Update
| -rw-r--r-- | CHANGES | 21 |
1 files changed, 12 insertions, 9 deletions
@@ -2,22 +2,20 @@ * Summary of Changes for Proof General 4.0 from 3.7.X -** Isabelle/Isar changes - -*** Electric terminator works without inserting terminator - - ** Generic changes *** XEmacs is no longer supported; PG only works with GNU Emacs 22.2+ *** Font-lock based Unicode Tokens mode replaces X-Symbol -*** Output retained for script buffer popups +*** Document-centric 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 "script centred" way of working, when output - buffers can be ignored and hidden. Disable auto raise for this. - Use full decoration to keep output when several steps are taken. + may enable a "document centric" 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) @@ -32,3 +30,8 @@ proof-electric-terminator-noterminator: allows non-insert of terminator +** Isabelle/Isar changes + +*** Electric terminator works without inserting terminator + + |