explicit locations for import_theory and setup_theory, for better user interface conformance

retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
tuned;

clarified scope of exception handlers;

relevant timing as in ML;
more PIDE modules;

more fundamental pred-to-set conversions for range and domain by means of inductive_set

merged

terminate after first exception -- avoid syslog flooding;

avoid buffer loading overrun;
tuned;

tuned whitespace

tuned import