more flexibile \setisabellecontext, independently of header;

prefer explicit heading command;

uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;

eliminated dead code;

clarified syntax -- avoid overlap with command category;

tuned signature (see ab2483fad861);

recover via scanner; tuned signature;

simplified -- scanning is never interactive;

tuned signature, in accordance to Scala version;

command-line terminator ";" is no longer accepted;

eliminated spurious semicolons;

eliminated former Proof General preferences;

merged

tuned;

provide explicit theory (amending 621c052789b4);

removed pointless markup; tuned comments;

discontinued obsolete \<^sync> marker;

discontinued obsolete control command category;

obsolete;

obsolete;

discontinued obsolete tty and prompt;

discontinued pointless option: timing is always on (overall theory only);

eliminated odd flags and hook;

avoid noise (cf. 03ff4d1e6784);