-*- 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 /BUGS first. --- * Summary of Changes for Proof General 3.5pre from 3.4 ** 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.