[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