[isabelle-dev] NEWS: more informative errors in lazy enumerations
makarius at sketis.net
Tue Nov 20 14:47:43 CET 2012
On Wed, 17 Oct 2012, Makarius wrote:
> 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.
The conclusion of this side-remark is now in Isabelle/599c935aac82:
apply_end stays as before, but there is a way to censor the command
completion table. I am not very fond of censorship, but there is no need
to encumber users by the full complexity of the history of Isar commands
that happens to be still active today.
Users can lead a happy live over several decades without ever getting
exposed to apply_end. And people who happen to know it and use it
occasionally, can easily type in the keyword as a whole.
More information about the isabelle-dev