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

[Makarius]

On Thu, 18 Jul 2013, Makarius wrote:

> On Thu, 18 Jul 2013, Florian Haftmann wrote:
>
>>>>> "Code generator: dropping subsumed code equation" by Auto Quickcheck
>>>> 
>>>>> I guess it would be the task the tools to omit such outbursts and not
>>>>> globally on the IDE side?
>>>> 
>>>> In principle Context_Position.is_visible should control that, and the
>>>> tools should observe it accordingly.
>>> 
>>> The canonical way to do that is
>>>
>>>   Context_Position.if_visible ctxt warning
>>> 
>>> but this does not work for code equations, because the operations of
>>> src/Pure/Isar/code.ML act on a global theory, which is always "visible"
>>> in that sense.
>
> 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.

One more amendment here: b824497c8e86 (I should not write emails while 
isabelle build is running).

The desastrous effects of HO unify traces, which where showing up here in 
solve_direct were mentioned on this thread started by Florian in 2009: 
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg00776.html

Interesting, because it is mainly about the critical transition from PG 
3.7.1.1 to PG 4.x and GNU Emacs 22 to 23 at that time.  Neither of that is 
of much relevance now, so it is fun to read about the old worries of 
getting *any* combination to work at all.


 	Makarius