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
|
Summary of Changes for Proof General 2.2 from 2.1
=================================================
Generic Changes
---------------
* New function C-c C-f (proof-find) to invoke some prover-specific
mechanism to search for theories.
* [XEmacs only] Toolbar has six new buttons (State, Context, Info,
Command, Help, Stop) which invoke commands previously available on
keys/menus. Also a new "Find" button for proof-find.
* [XEmacs only] Toolbar enablers have been added.
Buttons are automatically enabled or disabled as appropriate.
This requires XEmacs 20.4 or better for reliable working.
* Menus and keybindings have been reorganized.
Now keybindings invoke the same functions as the toolbar.
In particular, C-c C-n and C-c C-u are simplified so that
they always process or retract exactly one command, rather
than one command beyond point. Moreover, C-c C-u does not
take an optional argument to delete the retracted text
(it was too easy for the user to accidently type C-u C-c C-u !)
* Command C-c C-t (proof-try-command) removed in favour of C-c C-v
(proof-execute-minibuffer-cmd), which now uses the
filter proof-state-preserving-p to check that a command is safe.
* Terminal string now automatically added to command for C-c C-v
* [XEmacs only]
New function control-button1 (proof-mouse-track-insert) copies
individual commands (highlighted regions) from an open proof.
When a proof is closed, it behaves as mouse-track-insert
(the default XEmacs behaviour of control-button1).
* Switching scripting buffers is now more flexible.
When scripting is turned off in a partly-finished buffer,
the user is prompted whether to retract or process the buffer.
Automatic retraction or completion can be selected by
configuring the option proof-auto-action-when-deactivating-scripting.
(To be compatible with the file operations in a proof assistant,
Proof General only allows completely processed or completely
unprocessed scripts in non-active buffers).
* New function C-c C-s (proof-toggle-active-scripting) to switch
scripting on or off in current buffer. This is a handy way to
discard or finish off scripting in an unfinished buffer
triggering the deactivation mechanism mentioned above.
Switching on scripting in a buffer may cause the proof
assistant to load files it depends on, so it is also handy
to see what happens before scripting begins in the buffer.
* Cleaned up example files so all demonstrate same theorem "conj_comms".
Would be nice to add more theorems to compare scripts/proofs in
different systems. Please send in example scripts!
* Shorter buffer names for convenience.
* Removed transparent gif (text logo) from splash screen
because XEmacs can't display it nicely.
* Documentation updates.
Coq Changes
-----------
* Set proof-{qed,save}-commands so the toolbar functions work.
* Generic command C-c C-f (proof-find-theorems) replaces Coq
specific command C-c C-s (coq-Search).
Isabelle and Isar Changes
-------------------------
* Tweaks for input syntax.
* Recognize goals of the old form val prems = goal ...
Only in the developers' release
-------------------------------
* Provisional instantiation of Proof General for
Plastic (http://www.dur.ac.uk/CARG/plastic.html)
by Paul Callaghan <P.C.Callaghan@durham.ac.uk>.
Internal changes for developers to note
---------------------------------------
* Many robustness improvements so that Proof General fails
gracefully when certain configuration settings are unset.
The aim is to make it easier to adapt to new proof
assistants.
* proof-shell-leave-annotations-in-output variable has been added.
This allows quick and dirty mark up of output from the proof
assistant using special characters with codes above 128 and
font-lock. Such characters are hidden from display in the
output buffers.
However, it is NOT recommended to use this mechanism, because
it breaks the usability of cut and paste (which copies the
special characters). Furthermore the entire mechanism of
using special character codes is fragile and needs replacing
in future versions of Proof General!
* Renamed some configuration variables for uniformity:
proof-ctxt-string -> proof-context-command
proof-help-string -> proof-info-command
proof-prf-string -> proof-showproof-command
* Code cleanups and improvements.
|
