#298 (Apr 14, 2017, 12:50:11 AM)

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

Started by an SCM change

This run spent:

• 9.1 sec waiting;
• 1 hr 15 min build duration;
• 1 hr 15 min total from scheduled to completion.