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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Jul 18 12:20:02 CEST 2013

>>> "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.



PGP available:

-------------- 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>

More information about the isabelle-dev mailing list