more uniform schedule_theories, notably for "present" and "commit" phase after loading;

tuned;

moved more legacy to AFP

clarified modules;

clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);

tuned;

more thorough update of required files (amending 1529c3eb6bac);

clarified examples;

tuned proofs;

misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a);