Mon, 06 Mar 2017 18:28:48 +0100 | wenzelm | clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover); | changeset | files |
Mon, 06 Mar 2017 17:48:22 +0100 | wenzelm | more robust; | changeset | files |
Mon, 06 Mar 2017 17:10:37 +0100 | wenzelm | tuned; | changeset | files |
Mon, 06 Mar 2017 17:08:51 +0100 | wenzelm | proper Text.Range.offside (NB: in Scala ~1 == -2); | changeset | files |
Mon, 06 Mar 2017 17:05:57 +0100 | wenzelm | tuned; | changeset | files |
Mon, 06 Mar 2017 16:47:52 +0100 | wenzelm | more general tooltips, with uniform info range handling; | changeset | files |
Mon, 06 Mar 2017 11:48:06 +0100 | wenzelm | tuned; | changeset | files |