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