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