> BTW, http://proofgeneral.inf.ed.ac.uk/download still shows RC4.
Oops, committing web page failed -- will fix tomorrow, thanks for note. > +(if (and window-system (fboundp 'tool-bar-mode)) (tool-bar-mode t)) OK, this is likely to be contentious for Emacs experts who prefer the toolbar off and want some way to switch it off, or whoever made the odd decision in that Mac port to turn it off by default, but I'm not going to argue with you putting it in the Isar startup. It certainly is helpful for beginners. > 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. The first default should be robust now (a race condition was fixed in Trac #403). I've committed the second change. I've had other power users object to the mouse hovers and having trouble finding out how to switch them off, although it is in the user options menu. And given the assumptions made (still?) in Isabelle about trying things asynchronously when quiet mode is disabled we might as well have the speedier default. Besides, people will think that this kind of capability is only possible in jEdit then, 8-). - D. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
