Mon, 31 Mar 2014 12:16:35 +0200 | hoelzl | add rules about infinity of intervals | changeset | files |
Sun, 30 Mar 2014 21:24:59 +0200 | wenzelm | tuned proofs; | changeset | files |
Sun, 30 Mar 2014 21:03:40 +0200 | wenzelm | immediate completion even with delay, which is the default according to 638b29331549; | changeset | files |
Sun, 30 Mar 2014 20:23:26 +0200 | wenzelm | special treatment for various kinds of selections: imitate normal flow of editing; | changeset | files |
Sat, 29 Mar 2014 21:26:11 +0100 | wenzelm | merged | changeset | files |
Sat, 29 Mar 2014 20:41:50 +0100 | wenzelm | do not absorb vacuous copy operation, e.g. relevant when tooltip has focus but no selection, while the main text area has a selection but no focus; | changeset | files |
Sat, 29 Mar 2014 20:22:38 +0100 | wenzelm | check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component; | changeset | files |