shared output primitives of physical/virtual Pure;

shared thread position for physical/virtual Pure;

clarified bootstrap;

explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
handle bootstrap signatures as well;

more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;

clarified bootstrap;

clarified ML bootstrap;

--HG--
rename : src/Pure/ML/ml_pervasive_initial.ML => src/Pure/ML/ml_pervasive0.ML
rename : src/Pure/ML/ml_pervasive_final.ML => src/Pure/ML/ml_pervasive1.ML