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



On Wed, 19 Sep 2012, René Neumann wrote:

Now in PG 4.1 with GNU Emacs 23.x it seems that it never works: I see
only the initial askprefs by the prover, without any readjustments by
PG. This means that more basic things like quick-and-dirty also don't
work, i.e. it is off (the usual default of Isabelle), but Proof General
displays it as on, while leaving it de-facto off.

So in essence Isabelle states some setting being defaulted to, but
relies on an explicit message to actually set it to this default? And PG
4.x does not send this message anymore?

I don't know for sure. This part of PGIP is due to David Aspinall, both the older and newer behaviour.


	Makarius


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