Email Gateway (Aug 19 2022 at 11:23): Email Gateway (Aug 19 2022 at 11:23):From: Makarius <makarius@sketis.net>
Plugin Options / Isabelle / General / Editor Tracing Messages (default 1000).
Note that it is usually better to run tests in batch mode, although we
have recently managed to bomb the JVM with some AFP test going wild, and
producing hundreds of MB of funny tracing output. (Often tools break down
only when trying to be too verbose about their doings.)
Makarius
Email Gateway (Aug 19 2022 at 11:35):From: Walther Neuper <wneuper@ist.tugraz.at>
jEdit's recent limitation for output greatly improved the handling of
looping code.
Since we use jEdit like JUnit, i.e. have a "Test_Isac.thy" calling all
our test-files ---
(a) we get a great survey on errors by the red signs (=) at the left margin,
but
(b) we also get many many unpleasant request for interaction by
Tracing paused. Stop, or continue with next 100, 1000, 10000 messages?
Where in the abundant wealth of jEdit's menues can the buffer length of
Output be enlarged ?
PS: Isabelle2012 accepted Test_Isac.thy (but was inconvenient with looping)
Last updated: Nov 21 2024 at 12:39 UTC