Summary
- merged
- obsolete;
- clarified interactive mode, which is relevant for ML prompts;
- more careful print_depth on startup;
- ignore SIGINT in waiting wrapper process; proper "bash_process.c" and "build" within component;
- more robust cleanup; more defensive timing value;
- isabelle.Build uses ML_Process directly; isabelle_process is for batch mode only; removed unused feeder (already part of "isabelle console");
- tuned;
- print timing like lib/scripts/timestop.bash;
- prefer explicit locale;
- bash process with builtin timing;
- elapsed time in milliseconds (cf. Time.now in Poly/ML);
- support for timing of the managed process;
- tuned;
- proper support for RAW_ML_SYSTEM;
- 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;