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
|
-*- 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 ------
** Generic Changes
*** Menu reorganization, including new proof assistant specific menus.
Specific menus added for Coq, LEGO, Isabelle.
*** Favourites: user-defined commands added proof assistant specific menu
WORK ONGOING: PRESENTLY INCOMPLETE, DO NOT REPORT!
*** Proof assistant specific keymap added
Keybindings for proof assistant now begin with "C-c a".
*** Improved behaviour of electric terminator
*** Quick menu option to select proof-follow-mode
*** Point never moves if proof-follow-mode is 'ignore.
Previously it was always moved when an error occurred.
It's nicer to do this manually if you like this mode,
using M-x proof-goto-end-of-locked.
*** Efficiency improvement in parsing
Also works around crash bug in xemacs-21.1.7/SuSE.
Fix by Markus Wenzel.
*** Added possibility for switching prover's output on/off.
Already implemented in Coq and Isabelle(/Isar).
** 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
** Isar Changes
*** Fix for stack overflow in regexp which occurred with large proof states
** 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.
*** No need for match string 1 in proof-shell-proof-completed
*** Changed buffer mode name: pbp-mode -> proof-goals-mode, for uniformity.
|
