Changes

Summary

1. some NEWS (instead of proper documentation);
2. clarified signature;
3. simplified markup;
4. explicit setup of operations: avoid hardwired stuff;
5. clarified environment: allow "read>write" specification;
6. tuned;
7. tuned;
8. check environment name;
9. support named ML environments, notably "Isabelle", "SML"; more uniform options ML_read_global, ML_write_global; clarified bootstrap environment;
10. tuned;
11. tuned;
12. clarified signature;
13. clarified -- prefer new 'ML_export' command;