[isabelle-dev] Immediate completion does not work anymore
Makarius
makarius at sketis.net
Sun Nov 22 20:25:04 CET 2015
On Thu, 19 Nov 2015, Manuel Eberl wrote:
> As of the following revision, immediate completion does not work anymore in
> Isabelle/JEdit:
>
> changeset: 61600:1ca11ddfcc70
> user: wenzelm
> date: Sat Nov 07 16:05:28 2015 +0100
> summary: clarified completion of explicit symbols (see also f6bd97a587b7,
> e0e4ac981cf1);
>
> From the diff and the commit summary, I would very much assume that this is
> not an intentional change.
This belongs to the thread "NEWS: completion of explicit symbols", see
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-November/006407.html
Immediate completion should work exactly for non-word / non-backslash
abbreviations such as --> in a suitable context.
If there are other counter examples, I am still interested to see them.
Makarius
More information about the isabelle-dev
mailing list