empty abbrevs are removed globally;

tuned markup, e.g. relevant for Rendering.tooltip;

tuned message;

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;

report error on internal channel as well: startup_failure dialog may be too late;

clarified errors: more explicit treatment of uninitialized state;

check more files;

updated header;

tuned text

tuned