Changes

Summary

1. tuned: afford untyped/unscoped update;
2. more robust default: Scala imposes explicit "threads" value on ML, both the Poly/ML RTS and Isabelle/ML;
3. clarified signature: more explicit types/scopes;
4. tuned names;
5. tuned;
6. tuned documentation;
7. more robust: disallow empty clusters, so "isabelle build -H" really means cluster build;
8. clarified modules: centralize default policy;
9. more explicit types --- fewer warnings in IntelliJ IDEA;
10. tuned: avoid shadowing of names;
11. clarified default "isabelle build -j0 -H";
12. tuned whitespace;
13. clarifier worker vs. master, which may coincide for local build;
14. clarified signature: more standard defaults;
15. clarified signature;
16. clarified signature;
17. tuned;
18. prefer static object, while class is required for "services";
19. clarified signature: prefer default;