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
121c121
< (defcustom proof-strict-read-only 'retract
---
(defcustom proof-strict-read-only t
345c345
< (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.


        Makarius
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to