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

[Makarius]

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.


>> Maybe Florian also has some ideas about codegen.
>
> One answer would be to eliminate this meanwhile somehow ridiculous 
> warning entirely.

In principle you could refer to Context_Position.is_visible_global as 
well, but it looks all a bit complicated: quickcheck would have to pass 
down a modified theory, and code.ML would have to get all these lazy 
theory_ref things right.

Note that I am presently experimenting with a purely value-oriented theory 
type (Isabelle/38466f4f3483), where theory_ref is just an alias and 
Theory.copy / Theory.checkpoint just the identity.  So any mistakes in 
rearanging the theory_ref management in code.ML won't be detected at 
first, only if I have to backout 38466f4f3483 (e.g. due to resoure 
problems).


 	Makarius