[isabelle-dev] NEWS: asynchronous print functions etc.

[Makarius]

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:

changeset:   24178:4ff1dc2aa18d
user:        wenzelm
date:        Tue Aug 07 20:19:55 2007 +0200
files:       src/HOL/Bali/Basis.thy src/HOL/IMPP/Natural.thy 
src/HOL/Induct/Com.thy src/HOL/MicroJava/J/JTypeSafe.thy 
src/Pure/Isar/attrib.ML src/Pure/unify.ML 
src/Sequents/LK/Hard_Quantifiers.thy src/Sequents/ROOT.ML 
src/Sequents/Sequents.thy
description:
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 
visibility.


 	Makarius