[isabelle-dev] HOL/Library/Code_Prolog.thy breakdown

[Makarius]

Today isatest has reported a breakdown of HOL/Library/Code_Prolog.thy.

This was undetected in a more regular test due to this change that removed 
it from the normal HOL-Library session:

changeset:   38504:76965c356d2a
user:        haftmann
date:        Wed Aug 18 09:46:59 2010 +0200
files:       src/HOL/Library/ROOT.ML 
src/HOL/Tools/Predicate_Compile/code_prolog.ML
description:
removed Code_Prolog: modifies global environment setup non-conservatively


The mysterious modification of the global environment above was a 
redefined outer syntax command "values", with slightly different behaviour 
than the normal one.  Such a "poke" into the outer syntax affects the 
whole prover process, it escapes the context of the loaded theory and 
provokes erratic behaviour.

The ability to redefine outer syntax commands is merely an accidental 
left-over from the distant past.  It is required in interactive mode, to 
allow repeated processing of the (one!) command definition, but even that 
restricted scheme is apt to surprises as everybody knows.


So apart from some repairs of 
src/HOL/Tools/Predicate_Compile/code_prolog.ML in a76c679c0218, the 
changeset e42a3fc18458 makes more clear (in batch mode) that redefining 
outer syntax commands is not supposed to happen.  This provides a window 
of opportunity to remove spurious redefinitions elsewhere, until the 
coming release.

I might even come back to the global syntax table soon, and make it more 
conformant to Isabelle today, not 1998.  (It will require some special 
tricks to keep Proof General on board, because the old TTY loop somehow 
depends on the implicit state of the global syntax.)


 	Makarius