Summary
- recovered from Unicode accident in 7248d106c607;
- merged
- tuned -- fewer warnings;
- discontinued slightly odd "secure" mode;
- clarified Pretty.T toplevel pp;
- clarified modules;
- clarified modules;
- tuned header;
- clarified modules; tuned signature;
- @{make_string} is available during Pure bootstrap;
- clarified modules;
- unused;
- hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
- obsolete;
- tuned signature;
- obsolete;
- tuned whitespace;
- proper ML type;