simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;

tuned;

support named ML environments, notably "Isabelle", "SML";
more uniform options ML_read_global, ML_write_global;
clarified bootstrap environment;

clarified -- prefer new 'ML_export' command;

retain original PolyML.pointerEq;

prefer control symbol antiquotations;

clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;

proper type for Poly/ML development version;

avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;

more standard session build process, including browser_info;
clarified final setup of global ML environment;

shared output primitives of physical/virtual Pure;

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;

virtual thread data via context, for proper support of Context.>> etc;

clarified ML bootstrap environment;

--HG--
rename : src/Pure/ML_Root.thy => src/Pure/ML_Bootstrap.thy