Re: [isabelle] PG/Isabelle: Problem with Auto-Trace options (with workaround)
On Wed, 5 Sep 2012, René Neumann wrote:
(some of) the options set for Isabelle in ProofGeneral (like "Auto Solve
Direct", "Auto Quickcheck") are not active, even though they are
enabled. I don't know whether this bug lives in PG or in Isabelle...
Anyways: A normal workaround is to disable and enable these options
again in the menu -- which is cumbersome.
As far as I know this "feature" of Proof General has been always there in
the 4.x line of versions. You should put this on the regular Proof
General tracker and maybe also raise some attention on the Proof General
proofgeneral-devel mailing list.
I am myself no longer involved in Proof General maintenance since almost 1
year. Larry Paulson and Jasmin Blanchette have taken over
responsibilities to organize and motivate continued support for that
classic Isabelle interface.
Right now the few active people on the proofgeneral-devel mailing list
have switched into PG 4.2 release mode, so it is the right time to make
some progress, not just keeping the status quo (where the above issue is a
well-known part of).
This archive was generated by a fusion of
Pipermail (Mailman edition) and