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

[Peter Lammich]

On Di, 2012-11-20 at 14:47 +0100, Makarius wrote:
> 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.


Wouldn't it be better to just enumerate "censored" completions always
last in the completion list? Or are there technical difficulties to do
so?


> 
> 
>  	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev