blob: c55c1f1847a3defc38502191822b080c0b78ebf9 (
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
-*- 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
Unicode Tokens has been significantly improved since PG 3.7.1.
For best results, Emacs 23 is recommended.
*** 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.
*** 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.
This means that the editing, history and decoration inside the
proof shell (*coq*, *isabelle*, etc) are impoverished
compared with PG 3.X.
*** 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)
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'.
pg-insert-output-as-comment-fn: removed
proof-shell-wakeup-char: removed
proof-shell-prompt-pattern: removed
pg-use-specials-for-fontify: removed
proof-shell-strip-output-markup: required for cut-and-paste
proof-electric-terminator-noterminator: allows non-insert of terminator
*** 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
*** 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
|
