[isabelle-dev] PG preferences (auto solve in particular)

[Makarius]

On Wed, 11 Nov 2009, Florian Haftmann wrote:

> I'm currently asking myself whether the substructure of Isabelle 
> settings in the preferences menu is already carved in stone (although 
> only some adventurous people seem to be using PG 4 by now).
>
> In my naive view the distinction between "Display" and "Advanced 
> display" is quite artifical, whereas things like "Auto solve" and "Auto 
> nitpick" should be better placed in a separate menu "Hints".  Or is 
> there a rationale I am not aware of for the current categorization?

Without consulting the Mercurial history, I would say these categories 
were introduced by David Aspinall together with the first version of the 
formalized preferences concept (which is the only part of the Isabelle 
PGIP implementation that was ever used widely).

Before PG 4 the grouping of prefs is not directly reflected in the menus, 
so nobody noticed potential oddities.


Anyway, my may concern about PG 4 is to see it working at all.  There are 
many fundamental problems remaining.  Only two days ago I've found myself 
doing proofs with isabelle tty, because there was a Spontaneous Massive 
Existence Failure of PG 3.7.1 and PG pre-4 on Ubuntu 9.10, concerning 
Emacs 22 and 23 (Gtk).  (Those who are not following the Ubuntu or PG 
issue tracker, can use plain old emacs22-x until things are sorted out.)

IIRC, you are also using Ubuntu 9.10.  Which version of Emacs works for 
you?


 	Makarius