[isabelle-dev] ProofGeneral/PGIP spring cleaning

[Makarius]

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