Attentive readers of the changeset history may have already noticed the
current ProofGeneral/PGIP spring cleaning -- presently leading up to
Isabelle/bc0238c1f73a.
Thus the main ProofGeneral configuration is just one small file
src/Pure/Tools/proof_general.ML + some preferences in Pure and HOL. Being
back in a clean state that is easy to understand has various consequences:
* ProofGeneral preferences are just for ProofGeneral. The former
attempt to have PGIP preferences as standard prover options has been
discontinued. Isabelle/Scala system options have token over that role
in summer 2012 already.
* ProofGeneral startup involves regular Isabelle/Scala option
initialization, just like isabelle tty and jedit. Thus it
participates in the inherent advantages of Isabelle/Scala system
management, but also in JVM quirks: slow cold-start, occasional
surprises about inconsistent results from scalac (only relevant for
auto build from repository version of Isabelle).
* ProofGeneral preferences may have an optional "override" to enforce a
special value on startup, which may then be modified by the persistent
user preferences from the Emacs LISP environment. Thus the old
auto-quickcheck etc. problem introduced in the PG 4.x line has
disappeared. (Interestingly quick-and-dirty was also lost and is now
back, which might surprise some users.)
Generally the approach to Isabelle system integration is like this:
(1) Legacy Mode for vintage ProofGeneral usage (3.7.1.1 and 4.x)
without anything special nor new, just a certain status-quo.
(2) Standard Mode for using Isabelle/Scala for everything else by
default. That used to be avant-garde in 2008/2009, but is now
routine, despite Oracle, Apple, and other evil empires.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
