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

[Lars Noschinski]

On 31.03.2014 22:04, Makarius wrote:
>   - Syntax completion of the editor and semantic completion of the
>     prover are merged.  Since the latter requires a full round-trip of
>     document update to arrive, the default for option
>     jedit_completion_delay has been changed to 0.5s to improve the
>     user experience.
I haven't been able to get used to this (having to wait for a symbol
completion disturbs my typing flow), so I switched back to 0s. Enabling
immediate completion did not make this more palatable for me, for two
reasons: For example, "!" is not immediately completed (due to "!!").
Moreover, typos sometimes caused erroneous completions. I usually feel
that I mistyped and hit backspace immediately - if the word was
completed in between, I should have hit Ctrl-Z instead.

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.

  -- Lars