untyped, unscoped, unchecked access to JVM objects;
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
generate 'map_ident' theorem for BNFs
Documented new property
added lemma
note map_id0 more often
document 'map_id0'
tuned message: more compact, imitate actual command line;
tuned GUI;
tuned GUI;
tuned GUI;
some position markup to help locating the query context, e.g. from "Info" dockable;
no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;
tuned message;
merged
update for release;
bounce focus back to main text area -- Output is for output, not query input;
clarified detach_operation: ignore empty output;
tuned GUI;