[isabelle-dev] NEWS: asynchronous print functions etc.
makarius at sketis.net
Fri Jul 19 16:22:32 CEST 2013
On Fri, 19 Jul 2013, Tobias Nipkow wrote:
>> I have generalized the concept to allow changing the visibility of a
>> global theory context as well. This is observed by unify.ML, as a
>> guard to its many tracing options, find_theorems.ML then copies the
>> Proof.context visibility over to a copy of the background theory of the
>> goal state, so 'solve_direct' no longer produces spam from this source,
>> see Isabelle/d68fd63bf082.
> Does that mean that one could add an attribute unify_trace now?
These have been there since 2007:
date: Tue Aug 07 20:19:55 2007 +0200
files: src/HOL/Bali/Basis.thy src/HOL/IMPP/Natural.thy
turned Unify flags into configuration options (global only);
The "global only" aspect is a source of confusion and potential problems,
but it cannot be changed: unification is routinely applied without a
proper context, e.g. in "RS".
What I have done in 51dfdcd88e84 is to make
Context_Position.is_visible_global a guard for *any* output of the
unify.ML module -- it is quite complex in its chatty manner, and that way
we know that it cannot produce outbursts that bomb the prover front-end
for tools that can afford to change the global theory to disable context
More information about the isabelle-dev