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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
