Am 17/10/2012 11:09, schrieb 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. >
Excellent! > 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. I could never remember what apply_end was called and how to apply it although I frequently needed it. I did a quick test of the new behaviour and it does indeed seem to give the information that one really wants: which goals are left over (although it may take some staring at the left overs to figure out where they came from, but that was no better with apply_end). Hence I have no complaint if apply_end goes. Tobias > 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
