Tue, 07 Mar 2017 00:06:16 +0100 | wenzelm | maintain decorations for document (model) and update it for each editor (view); | changeset | files |
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 |