#76 (Mar 9, 2016, 9:59:09 PM)

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

Started by an SCM change