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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
