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
|
-*- 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
** Generic changes
*** Bundling of X-Symbol Mode (4.45 beta)
!!THIS IS WORK IN PROGRESS, IT MAY WELL BREAK X-SYMBOL FOR YOU!!
To disable use of the bundled version, simply delete or move away
the x-symbol subdirectory.
*** Bundling of MMM Mode (for multiple modes in one buffer)
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.
Contributions of configuration for other provers welcomed.
*** X-Symbol (and MMM-mode) minor mode behaviour simplified
These minor modes like to be responsible for turning themselves
on and off. PG does not anymore try to synchronise the on/off
settings in all PG buffers (which could lead to half an hour
of fontification!). Instead the menu reflects the current
minor mode status; toggling it will also update the default
"global for PG" behaviour for new script buffers.
*** 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]
** 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.
** Changes for Isabelle
Beginnings of support PGIP protocol (work in progress with Isabelle
CVS version). Presently allows Isabelle to configure Proof General.
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.
|
