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

[Florian Haftmann]

>>> "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.
> 
> Maybe Florian also has some ideas about codegen.

One answer would be to eliminate this meanwhile somehow ridiculous
warning entirely.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130718/af7aae39/attachment.sig>