On Wed, 21 May 2014, Lars Noschinski wrote:
The other thing I noticed during the last days was the following: When I
modify a term, I usually place the term at the position where I want to
insert something (which is often directly before a variable or
constant), start typing and only add the necessary space as the last
character I type. This means that I don't have symbol completion
available (because the completion mechanism believes me to be in the
middle of a word). I usually notice this when I want to enter a symbol,
so I type SPACE LEFT and add another character of the symbol to trigger
the completion popup.
I changed that again, see 0f708666eb7c and ff31aad27661 with many more
history references in the changelog.
That means: symbol completion works within a word context, but keyword
completion not.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
