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;