Mon, 24 Feb 2014 13:16:50 +0100 | wenzelm | tuned messages -- prefer quote before Position.here, which might be just \<here>; | changeset | files |
Mon, 24 Feb 2014 13:10:33 +0100 | wenzelm | clarified ML language flags; | changeset | files |
Mon, 24 Feb 2014 12:51:55 +0100 | wenzelm | clarified painting of invisible caret, e.g. focus change due to popup; | changeset | files |
Mon, 24 Feb 2014 12:23:35 +0100 | wenzelm | tuned signature -- weaker type requirement; | changeset | files |
Mon, 24 Feb 2014 12:14:03 +0100 | wenzelm | paint completion range of active popup; | changeset | files |
Mon, 24 Feb 2014 11:05:02 +0100 | wenzelm | tuned messages; | changeset | files |