*** 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
