[isabelle-dev] NEWS: asynchronous print functions etc.
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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev