[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