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

[David Greenaway]

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:

    editor_tracing_messages

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

Sorry for the noise.

David

--




________________________________

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.