Changes

Summary

1. tuned whitespace;
2. more careful quoting for the sake of Windows;
3. tuned;
4. tuned;
5. tuned signature;
6. more direct invocation of ISABELLE_BASH_PROCESS on Windows;
7. tuned signature;
8. tuned signature;
9. updated bash_process;
10. actually wait for forked process and return its status -- this is not meant to be a daemon;
11. tuned signature;
12. tuned signature -- more like ML version;
13. suppress empty messages as in ML;
14. clarified bash process -- similar to ML version;
15. clarified bash process;
16. tuned according to ML version;
17. clarified name;
18. more flexible command-line; flush before exit/fork/exec, to make double sure that output is shipped;
19. tuned signature;