[isabelle-dev] NEWS: more informative errors in lazy enumerations

[Makarius]

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