more systematic Isabelle output, like in classic Isabelle/ML (without markup);

explicit Exn.error_message in accordance to Output.error_message in ML;

clarified message and return code, in accordance to ML version;

tuned;

tuned imports;

support for more informative crashes;

more general support for Isabelle/Scala command line tools;