| 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 |
| Wed, 20 Jan 2016 23:19:52 +0100 | wenzelm | check more files; | changeset | files |