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

[Makarius]

On Mon, 15 Jul 2013, Makarius wrote:

> On Mon, 15 Jul 2013, Dmitriy Traytel 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.  (Such flags cannot be changed on the background theory on the 
fly, because it would extend that according to Theory.subthy and thus 
affect derived results.)

I have a slightly different plan to silence solve_direct, with its global 
unify trace options: depending on Context_Position.is_visible these will 
be reset, on a different (auxiliary) theory that is used for the 
exploration only.

Maybe Florian also has some ideas about codegen.


Now that things start to look nice in the Prover IDE, the old somewhat 
crude message output becomes more apparant.  Standards are higher today 
than several years ago.


 	Makarius