On 21/01/13 23:08, Makarius 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?
The longest unification-related tracing messages I witnessed in our proofs were a little under 1500 lines (I saw three such cases). There were tens of proofs producing between 100 and 1000 lines. Testing on my own machine, viewing 10,000 lines of tracing output appears to work without any problems. When I hit a little above the 30,000 mark though, I start to see strange behaviour where the output buffer fails to display any output. I think a value of at least 1000 would be a sensible default; I am not sure what value between 1000 and 10,000 lines would be best, though. Thanks so much, 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
