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
|
-*- outline -*-
--- This is a development release of Proof General, ---
--- some features may be incomplete or buggy. Please ---
--- report any problems to support@proofgeneral.org, ---
--- thanks. Check files BUGS and <prover>/BUGS first. ---
* Summary of Changes for Proof General 3.5pre from 3.4
*** Bundling and configuration for Multiple Modes (MMM-Mode)
MMM mode allows submodes to be used in the same file.
See http://mmm-mode.sourceforge.net/.
At present it is configured for Isar, to allow LaTeX and
sml-mode to be used inside Isar scripts.
** GNU Emacs compatibility, simplified font-lock, handling nested comments
*** Numerous improvements, thanks due to Stefan Monnier.
*** Some GNU Emacs backwards compatibility removed: use 21.1 or later
*** PROBLEMS REMAINING: Menu problems currently on 21.2, may affect loading.
Temp fix: turn on mode manually first in *scratch* buffer, then
visit file.
** Generic changes
*** Follow mode: add "followdown" setting
In this mode, the point moves with the locked region when it moves
down in the buffer (processing). For undo, the point does not move.
*** Options and proof assistant settings improvements
Facility to reset to default values added, and saving
of (just) proof assistant settings.
*** Display management: added shrink-windows-tofit option
Attempt to shrink output windows to fit their contents in
case it is less than 1/2 the window height. In progress.
*** Parsing internals changed: minor user visible differences
Please report any problems/annoyances which may be unexpected.
NB: Not yet enabled for Isabelle/Isar.
*** Tweaks to menus, colours
Electric terminator menu option more visible.
Reduce contrast for mouse highlighting of regions.
*** Support formatted input which contains newlines [for Coq]
A patch from Stefan Monnier, to allow Coq input to have newlines
remaining, so that input formatting is not broken. A much better way
to address this would be to alter the Coq output routines so that they
do not print multiple identical prompts for continued lines.
[this is in testing: please notify me of problems in other provers]
** Changes for Isabelle
Beginnings of support PGIP protocol (work in progress with Isabelle
CVS version). Presently allows Isabelle to configure Proof General.
CURRENTLY SUPPORT FOR CURRENTLY RELEASED ISABELLE VERSIONS IS BROKEN!
Backward compatibility may not be maintained: it's simply too much
effort. This means that if you upgrade your Emacs version, which
forces you to upgrade Proof General because Emacs upgrades usually
break Proof General (Emacs authors pay little heed to maintaining
APIs), then you may have to upgrade your Isabelle version as well.
|
