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

[Makarius]

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.


 	Makarius