| Sat, 23 Jan 2016 11:52:48 +0100 | wenzelm | empty abbrevs are removed globally; | changeset | files |
| Fri, 22 Jan 2016 14:46:02 +0100 | wenzelm | tuned markup, e.g. relevant for Rendering.tooltip; | changeset | files |
| Thu, 21 Jan 2016 22:16:48 +0100 | wenzelm | tuned message; | changeset | files |
| Thu, 21 Jan 2016 21:12:45 +0100 | wenzelm | more robust initialization: createMenu(_, null) is called early (during EditPane creation), thus it precedes the startup_failure dialog and could crash if PIDE.options are uninitialized; | changeset | files |
| Thu, 21 Jan 2016 20:57:37 +0100 | wenzelm | report error on internal channel as well: startup_failure dialog may be too late; | changeset | files |
| Thu, 21 Jan 2016 20:50:34 +0100 | wenzelm | clarified errors: more explicit treatment of uninitialized state; | changeset | files |