Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround)



On Thu, 20 Sep 2012, René Neumann wrote:

And as far as I see it, the defaults of boolean preferences are the actual values of the variables. Hence this should be ok. BUT: Some preferences are set in an Unsynchronized.setmp block which cancels this assumption.

Yes, these setmps are the right thing in terms of the classic interpretation of PGIP askprefs/setpref messages -- whatever that was exactly. You still have that classic behaviour in ProofGeneral-3.7.1.1, which is still the standard version of many Proof General users.

Before changing anything on the Isabelle side, I need an explanation if PGIP has changed in recent years, or if it is just an accident of the PG-4.x line.

This is particularly relevant since I am about to revisit the PGIP preferences implementation soon, to unify it with the standard Isabelle options/preferences mechanism that will be in the next release. Otherwise the "fix" will become loose again and just fall off.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.