merged

tuned output;

tuned comments;

clarified signature; clarified modules;

tuned;

avoid tmp files to improve robustness on Windows, where ERROR_PATH_NOT_FOUND has been seen (see also 569135d7352a);

tuned signature: more operations (following Isabelle/Scala);

more operations;

clarified signature: re-use existing Process_Result.T (NB: err_lines are de-facto program startup errors, anything else is redirected to out_lines);

tuned signature: more explicit operations;

tuned output;

misc tuning;

tuned Isabelle/ML: more uniform semicolons;

clarified signature: scalable Bash.input thanks to Bytes.T;

added time_partial_function command

A couple of theorems proved by Manuel Eberl from his AFP entry Sum_Of_Squares_Count

tuned;

tuned;

tuned signature;

proper Path.print for user output (amending 9498623b27f0);

tuned signature: more concise access to context data;

tuned English prose;

merged

tuned;

more uniform cleanup;

tuned messages;

more robust: avoid expand_path, which requires "bin/isabelle getenv"; more concise: just one ssh command; more thorough: delete etc/preferences as well;

NEWS;

enforce fresh build of HOL-Codegenerator_Test;

more platforms (untested);