> 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 

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

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to