Changes

Summary

1. for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
2. early abort on depth limit
3. obsolete
4. tuned
5. merged
6. clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
7. clarified directories;
8. tuned signature (again);
9. proper bootstrap base for building Pure;
10. tuned according to Scala version;
11. more global theories;
12. tuned;
13. clarified loaded_theories: map to qualified theory name; proper theory_name for PIDE editors;
14. global session_base for PIDE interaction;
15. more explicit jEdit file operations; less redundant JEdit_Resources.node_name();
16. early check and normalization of session directory, e.g. relevant for path information passed to ML process, which may have a different CWD;
17. tuned;
18. tuned
19. more fundamental euler's totient function on nat rather than int; avoid generic name phi; separate theory for euler's totient function