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 > [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
