use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader; tuned signatures;

clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;

tuned;

clarified bootstrapping of Pure;

tuned errors;

prefer File.full_path in accordance to check_file;

more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;

updated Thy_Load.check_thy;

refined Thy_Load.check_thy: find more uses in body text, based on keywords; refined Thy_Info.require_thy(s): cumulate additional keywords; slightly more value-oriented type Keywords.keywords;

more direct cumulation of (sparse) keywords; discontinued slightly odd patching of Pure keywords; tuned signature;

some support for thy_load_commands; clarified signatures;

tuned signature;

clarified initialization of Thy_Load, Thy_Info, Session;

tuned;

more robust cleaning of "% tag" and "-- cmt";

some support for inlining file content into outer syntax token language;

tuned comment;

tuned;

added keyword kind "thy_load" (with optional list of file extensions);

updated generated files;

more strict syntax, according to manual;

abstracted lemma

retain unknown options within preferences; tuned print;

more comprehensible platform family name;

tuned message;

fewer components, more roots;

actually remove makeall (cf. 292b97e17fb7);

tuned;

Backed out changeset ec82c33c75f8;

Typo fixed.