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

[Lars Noschinski]

On 31.03.2014 22:04, Makarius wrote:
> These cumulative NEWS refer to Isabelle/075397022503.  This also marks
> the point where my continously shrinking and growing TODO list has
> reached a stable state concerning "completion" and the main activity
> on this part is finished for now.

I have recently written some proof with some german plain text. This
triggered a lot of completion popups, suggesting to correct german to
english words (which is to be expected). Unfortunately, the completion
popup does not disappear when I continue typing the next word. Then, at
the end of the line, i press RETURN TAB (to get to the correct
indentation level again) which then completes the word -- this seems to
be timing related, as a single RETURN <pause> closes the completion popup.

For me, the expected behaviour would have been to close the completion
as soon as a word-separating character (in this case, a space) has been
entered.

  -- Lars