Changes

Summary

1. merged
2. obsolete;
3. clarified interactive mode, which is relevant for ML prompts;
4. more careful print_depth on startup;
5. ignore SIGINT in waiting wrapper process; proper "bash_process.c" and "build" within component;
6. more robust cleanup; more defensive timing value;
7. isabelle.Build uses ML_Process directly; isabelle_process is for batch mode only; removed unused feeder (already part of "isabelle console");
8. tuned;
9. print timing like lib/scripts/timestop.bash;
10. prefer explicit locale;
11. bash process with builtin timing;
12. elapsed time in milliseconds (cf. Time.now in Poly/ML);
13. support for timing of the managed process;
14. tuned;
15. proper support for RAW_ML_SYSTEM;
16. tuned signature;
17. separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
18. back to external line editor, due to problems of JLine with multithreading of in vs. out;
19. ignore execeptions that usually occur due to shutdown;
20. clarified initial ML;
21. isabelle console is based on Isabelle/Scala;
22. clarified process interrupt: exactly one signal (like thread interrupt);
23. tuned signature;
24. 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;
25. removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;
26. prospective command line entry point for simplified isabelle_process;
27. tuned signature;
28. proper Path.print for user messages;
29. discontinued cd, pwd;
30. tuned -- more standard operations;
31. 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;
32. clarified treatment of DEL; tuned signature;
33. clarified RAW_ML_SYSTEM;
34. tuned;
35. 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);
36. manage the underlying ML process in Scala;
37. clarified modules;
38. tuned signature;