[isabelle-dev] NEWS: improved syntactic and semantic completion mechanism

[Makarius]

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