[isabelle-dev] NEWS: asynchronous print functions etc.
Makarius
makarius at sketis.net
Mon Jul 15 16:57:14 CEST 2013
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. I will take a few more rounds of
looking at the current collection of tools we have right now; solve_direct
should be also able to contain itself, without too much spamming.
Makarius
More information about the isabelle-dev
mailing list