CHANGES


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

-*- 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

** GNU Emacs compatibility, simplified font-lock, handling nested comments

*** Numerous improvements, credit to Stefan Monnier.


** Generic changes

*** 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