tuned signature;

separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";

back to external line editor, due to problems of JLine with multithreading of in vs. out;

ignore execeptions that usually occur due to shutdown;

clarified initial ML;

isabelle console is based on Isabelle/Scala;

clarified process interrupt: exactly one signal (like thread interrupt);

tuned signature;

more abstract Session.start, without prover command-line; Isabelle_Process.apply is directly based on ML_Process; clarified Isabelle_Process.main command-line; tuned signature;

removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;

prospective command line entry point for simplified isabelle_process;

tuned signature;

proper Path.print for user messages;

discontinued cd, pwd;

tuned -- more standard operations;

File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; clarified treatment of whitespace in some bash scripts;

clarified treatment of DEL; tuned signature;

clarified RAW_ML_SYSTEM;

tuned;

Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined; more robust File.bash_escape; more robust treatment of ML_OPTIONS; clarified prover args (again);

manage the underlying ML process in Scala;

clarified modules;

tuned signature;

Merge