Changes

Summary

1. more Isabelle/ML/Scala operations;
2. more Isabelle/ML/Scala operations;
3. more Isabelle/ML/Scala operations; clarified errors;
4. proper src1, amending 20157c8ab3f3;
5. tuned;
6. proper File.eq, amending df49ca5da9d0;
7. tuned;
8. clarified modules: more like ML;
9. obsolete;
10. tuned;
11. more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
12. discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working;
13. more checks;
14. clarified message;
15. clarified message;
16. clarified comments;
17. clarified message;