simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database;
Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command;
added Thy_Load.begin_theory for clarity;
structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader;
moved some basic commands from isar_cmd.ML to isar_syn.ML;
misc tuning and simplification;