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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
-*- outline -*-
* Main Changes for Proof General 4.0 from 3.7.1
** Install/support changes
*** XEmacs is no longer supported; PG only works with GNU Emacs 22.2+
*** 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.
** Generic changes
*** 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.
See Tokens menu for many useful commands.
*** 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 the prover 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.
*** Automatic processing mode
Quick Options -> Send Automatically
Sends commands to the prover when Emacs is idle for a while.
This only sends commands when the last processing action has
been an action moving forward through the buffer. Interrupt by
making a keyboard/mouse action.
*** Fast buffer processing option
Quick Options -> Fast Process Buffer
This affects 'proof-process-buffer' (C-c C-b, toolbar down).
It causes commands to be sent to the prover in a tight loop, without
updating the display or processing other input. This speeds up
processing dramatically on some Emacs implementations.
To interrupt, use C-g, which reverts to normal processing mode.
(To stop that, use C-c C-c as usual).
*** Improved prevention of Undo in locked region
With thanks to Erik Martin-Dorel and Stefan Monnier.
Undo in read only region follows `proof-strict-read-only' and
gives the user the chance to allow edits by retracting first.
*** Proof General -> Options menu extended and rearranged
- new menu for useful minor modes indicates 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)
*** "Movie" output: export an annotated buffer in XML
Basic movie output for Proviola, see http://mws.cs.ru.nl/proviola
*** 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)
*** Simplified version of comint now used for proof shell (internal)
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.
** Isabelle/Isar changes
*** Support undo back into completed proofs (linear_undo).
*** Electric terminator works without inserting terminator
Hit ; to process the last command. Easier than C-RET.
*** 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
|
