On Wed, 17 Oct 2012, Peter Lammich wrote:
On Mi, 2012-10-17 at 11:09 +0200, Makarius wrote:
*** ML ***
* Type Seq.results and related operations support embedded error
messages within lazy enumerations, and thus allow to provide
informative errors in the absence of any usable results.
Cool, no more writing of error messages to the trace buffer when
debugging tactics.
It probably does not help here:
On Wed, 17 Oct 2012, Makarius wrote:
note that plain tactics are inherently restricted to the classic failure
and backtracking model without error messages.
BTW, the trace buffer is only relevant for Proof General in order to get
messages past its built-in filtering and priority model of
writeln/warning/error. In Isabelle/jEdit you would just use plain writeln
by default and then inspect the output or hover over the squiggles in the
source.
Tracing did get a new meaning in Isabelle/jEdit recently, when I
introduced some means to restrict its volume at the very source of the
message stream. Thus a simp trace gone wild would just expire the command
transaction. For example in Isabelle/b0d6d2e7a522:
declare [[simp_trace]]
datatype foo = Foo | Bar foo
This gives you 0.5 MB of message content -- 184 Tracing messages shown in
the Output window if the radio button is enabled -- and finally some error
"Tracing limit exceeded: 509725" before any further harm is done.
This is a relatively cheap trick to address an ancient problem. I would
be interested to hear from early adopters how it works out in hard work.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
