merged

clarified empty merge; tuned;

permissive loaded_theories (amending 67dbf5cdc056): user errors are produced e.g. in Known.make;

prefer native platform x86-windows, to make this work on x86_64-cygwin;

tuned signature;

even more robust syntax (amending 122df1fde073);

clarified error for bad session-qualified imports;

clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;

merged

completion supports theory header imports; tuned;

clarified modules;

tuned signature;

new theorem at_within_cbox_finite

process ROOT files only once, which allows duplicate (or overlapping) session root directories;

prefer Cygwin64, although some components still require update;

updated test version;

more recent polyml-test version;

misc tuning and modernization;

discontinued obsolete 'files' in session ROOT;

prefer file dependencies wrt. specific theories;

added command 'external_file';

proper document (cf. 9f5bfef8bd82);

removed pointless dependencies: done by 'spark_open';

merged

more documentation;

clarified imports: prefer parent session images;

eliminated old-style no-document imports;

proper document;

more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;

more documentation;