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

[Makarius]

*** 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.


*** General ***

* More informative error messages for Isar proof commands involving
lazy enumerations (method applications etc.).


This refers to Isabelle/bd370af308f0.  The latter application means that 
the laconic "empty result sequence" should hardly ever happen again in 
practice -- it depends on the proof command implementation how nice the 
error message becomes.  Some more hot spots of the system may be brushed 
up eventually, but note that plain tactics are inherently restricted to 
the classic failure and backtracking model without error messages.


Side remark:

Does anybody remember a use of the 'apply_end' command? Many years ago it 
was introduced to help analyse the failure of 'qed', in symmetry to 
'apply' to break up 'proof' and 'by' steps.  That should now work without 
it, just by letting 'qed' crash and looking at the error message.  Of 
course, 'apply' has other uses and is not affected here.

Myself I've almost forgotten about 'apply_end', before constantly reminded 
of its existence by the Isabelle/jEdit completion, which proposes it when 
the user tries to write 'apply'.  So there is a clear motivation to get 
rid of the old 'apply_end' feature.


 	Makarius