tuned: afford untyped/unscoped update;

clarified signature: avoid ill-defined type java.net.URL;

unused;

tuned: afford untyped/unscoped update;

more robust default: Scala imposes explicit "threads" value on ML, both the Poly/ML RTS and Isabelle/ML;

clarified signature: more explicit types/scopes;

tuned names;

tuned;

tuned documentation;

more robust: disallow empty clusters, so "isabelle build -H" really means cluster build;