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 MHonArc.