On Fri, 16 Sep 2011, David Aspinall wrote:

There is a new release candidate available now (RC5) which contains the recent (mainly Coq-related) fixes. I hope this will be the last RC and not contain show stoppers!

OK, I will include RC5 in the next Isabelle test bundle that should be published within the next few days.

BTW, http://proofgeneral.inf.ed.ac.uk/download still shows RC4.

BTW 2, in Isabelle2011 we've had some adhoc patches for the 4.1pre version that was included. I have already applied the following to the PG CVS just after RC5:

brute-force method to enable tool-bar-mode, which is especially important on GNU Emacs for Mac OS X (change was already present in Isabelle2011);

diff -r 794ea4230dfb -r 7947bb2b3fd3 isar/interface-setup.el
--- a/isar/interface-setup.el   Fri Sep 16 10:00:13 2011 +0000
+++ b/isar/interface-setup.el   Sat Sep 17 15:03:27 2011 +0000
@@ -11,6 +11,12 @@

+;; Tool bar
+(if (and window-system (fboundp 'tool-bar-mode)) (tool-bar-mode t))
 ;; Unicode

The remaining differences are as follows:

diff -r ProofGeneral-4.1pre101216/generic/proof-useropts.el ProofGeneral-4.1pre101216-p1/generic/proof-useropts.el
< (defcustom proof-strict-read-only 'retract
(defcustom proof-strict-read-only t
< (defcustom proof-full-annotation t
(defcustom proof-full-annotation nil

My tendency is to ignore the latter and ship PG 4.1 final as is.

ProofGeneral-devel mailing list

Reply via email to