[isabelle-dev] NEWS: more informative errors in lazy enumerations
lammich at in.tum.de
Tue Nov 20 15:05:28 CET 2012
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
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev