blob: db67878ec5be15568bfff8443de5b7b5bafa0e7d (
plain)
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
|
-*- outline -*-
* 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
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.
*** 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
|