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



Am 19.09.2012 14:41, schrieb Makarius:

> I think the deeper probelm is a misunderstanding what the PGIP messages
> "askprefs" vs. "setpref" mean, notably the "default" field of "askprefs".
> 
> In classic ProofGeneral-3.7.1.1 / XEmacs 21.4, the prover would report
> static defaults stemming from "askprefs", and Proof General react with
> further "setpref" messages to adapt to the dynamic values on either
> side, such that the persistent preferences from Emacs are transferred to
> the prover at run time.
> 
> In PG 4.0 or so, it would depend on the Emacs version if this worked out
> or not.
> 
> 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?

> This discussion should probably continued on the above PG trac thread

So I may paste your message there?

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055





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