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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
-*- outline -*-
* Summary of Changes for Proof General 3.2 from 3.1
----- NB: this is a pre-release of PG 3.2. Bugs likely, please report ------
----- PG 3.2 is scheduled for release at the end of September 2000. -----
** Generic Changes
*** Keybindings alterations
Keybindings for proof assistant now begin with "C-c C-a", to make more room.
*** Menu reorganization, including new proof assistant specific menus.
Menu layout more consistent and convenient (though larger).
Specific menus added automatically for each proof assistant.
(Additional content in specific menus added for Coq, LEGO, Isabelle).
Menus appear in goals and response buffers too.
*** Toolbar added to response and goals buffer in single frame mode.
Disappearing toolbar was a source of confusion for novice Emacs users.
Also better for proof-by-pointing interactions.
*** Toolbar and menubar removed from small windows in multiple frame mode
More screen real estate for your windows. (XEmacs only)
*** Favourites: user-defined commands can be added to PA specific menus.
*** Improved behaviour of electric terminator
*** Proof-follow-mode: quick menu option, improved 'ignore behaviour.
Previously point was always moved when an error occurred.
It's nicer to do this manually if you like the 'ignore mode,
using M-x proof-goto-end-of-locked (C-c C-.)
*** Added handy proof-display-some-buffers (C-c C-l)
This displays the response or goals buffer, and toggles between
them in two-pane mode. In three-pane or multiple frame mode,
it makes sure both response and goals buffer are visible.
*** Added proof-next-error function, bound to C-c `
When the proof assistant batch loads files "in the background"
rather than incrementally via script management, error messages
may appear in the response buffer with file/line numbers.
Proof General can now parse these messages to jump to the
location of the error.
[Currently implemented for: Isabelle]
*** New more efficient and generalised parsing functions
The new functions have slightly different behaviour around comments.
Also avoids crash bug with long strings in certain XEmacs versions.
*** New indentation code, indentation enabled for all provers now
Supplied by Markus Wenzel.
*** Added possibility (internal) for switching prover's output on/off.
Already implemented in Coq and Isabelle(/Isar).
This improves efficiency by giving more CPU to prover.
*** Makefile has new target "scripts" to adjust paths in bash/perl scripts
*** Solaris/Windows turn off toolbar enablers due to problems.
*** Bug fix: "next" button enabled more often.
*** Bug fix: first line ignored problem fixed for Coq and others.
[Developers note: to fix this properly, we have added
`proof-shell-pre-sync-init-cmd' for provers that need initialization
before synchronization can be secured. LEGO needs to wait for
second prompt before sync, whereas Isabelle managed to sync on first
prompt. Coq was best, with sync set before startup, using a command
line option. That is the recommended route for new proof assistants.]
*** Bug fix: script management is now more robust against C-x C-v, C-x C-w
Please let me know of any cases where this fails.
** Coq Changes
*** More decoration of Coq output, uses CoqResp mode now
** LEGO Changes
*** Slight change in output during proof: shows final discharge messages
This is a side effect of code rationalization in PG elsewhere.
** Isabelle Changes
*** More code from Isamode has been merged into Proof General
Particularly: the user now can choose a logic image from inside PG.
*** Fix for stack overflow in regexp which occurred with large proof states
*** The back() command is now undoable as it should be
** Isar Changes
*** No longer requires explicit terminators ";" in text. (XEmacs only)
Also note that isar-strip-terminators cleans up existing theories.
*** Fix for stack overflow in regexp which occurred with large proof states
*** Improved Help menu provides basic context browsing facilities.
** HOL Changes
*** Output decoration improvements.
** Changes for developers to note
*** Rearrangement of elisp files and loading mechanism.
Autoloads in proof-autoloads.el are generated from
;;;###autoload comments with `make devel.autoloads'
Several new files, to "modularize" the code a bit more.
*** New mechanism for defining customizations per prover
See Section 9 of proof-config.el. New macros mean that we can
write for example `proof-defasscustom web-page' to automatically get
`isa-webpage', `hol-webpage', etc, declared on loading.
Proof assistant specific code can then just set/use these
variables, without needing to set `proof-assistant-webpage' from
`isa-webpage' etc.
This slightly breaks the original pseudo object-oriented idea
behind the instantiation mechanism (overriding methods, setting
attributes) but works much more smoothly with customization.
*** Changed buffer mode name: pbp-mode -> proof-goals-mode, for uniformity.
*** Removed proof-terminal-string to simplify command setting
As a simplification of the code, and to allow possibility of
PAs without a terminal string, more smoothly.
It is now the responsibility of each proof assistant's customization
to add proof-terminal-string to commands where necessary.
*** New parsing mechanism
See the PG Adapting manual for information about the new variations
possible for `proof-segment-up-to'. These are supported for XEmacs only,
since FSF Emacs lacks the useful fast primitives we use.
*** Other minor things (interest only to independent developers of PG modes):
No need for match string 1 in proof-shell-proof-completed
Added proof-shell-pre-sync-init-cmd, see doc.
|
