[isabelle-dev] "Tracing paused" messages undesirably cause proofs running in background to stall

Makarius makarius at sketis.net
Mon Jan 21 13:08:00 CET 2013


On Fri, 18 Jan 2013, David Greenaway wrote:

> After inspecting the Isabelle source a little more, I have seen that
> there is a jEdit configuration variable:
>
>   editor_tracing_messages
>
> that allows the pause threshold to be adjusted. Setting this value to a 
> large number solves my first problem.

The question might be as simple as providing a good default.  In 
Isabelle2013-RC1 it is 100 messages, which is probably about low.  How 
about 1000?  Would that make your theories run through unhindered?


 	Makarius




More information about the isabelle-dev mailing list