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

David Greenaway david.greenaway at nicta.com.au
Fri Jan 18 07:29:16 CET 2013

On 18/01/13 16:49, David Greenaway wrote:
> One minor problem I am hitting is the "Tracing paused" messages when
> running proofs interactively. More precisely, when a tactic (or similar)
> generates too much output using the "tracing" command, the following
> message is displayed:
>      Tracing paused.  Stop, or continue with next 10, 100, 1000 messages?
> Clicking on one of the numbers listed in the message allows more tracing
> messages to be displayed, and the tactic to continue.
> While the unification eventually succeeds, each such proof statement
> requires human interaction in order to be processed.

After inspecting the Isabelle source a little more, I have seen that
there is a jEdit configuration variable:


that allows the pause threshold to be adjusted. Setting this value to
a large number solves my first problem.

Sorry for the noise.




The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

More information about the isabelle-dev mailing list