#1592 (Nov 7, 2021, 12:50:10 AM)

1. cover all possible kinds, notably for references outside of this theory (amending 129fb11b357f); (detail / hgweb)
2. proper foundational order; (detail / hgweb)
3. back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition"; (detail / hgweb)
4. use all entity kinds from theory export, e.g. "method", "attribute"; (detail / hgweb)
5. clarified signature; (detail / hgweb)
6. clarified physical_ref; (detail / hgweb)
7. proper treatment of session build hierarchy; (detail / hgweb)
8. proper used_theories for session build hierarchy, not known_theories from imported sessions; (detail / hgweb)
9. present theories from imported sessions as required; (detail / hgweb)
10. avoid multiple copies of fonts;
    proper fonts prefix for aux. files; (detail / hgweb)
11. more compact persistent data; (detail / hgweb)
12. tuned; (detail / hgweb)
13. proper term_cache; (detail / hgweb)
14. prefer "NAME|KIND" format, as already used in Isabelle/MMT and Isabelle/Dedukti; (detail / hgweb)
15. tuned; (detail / hgweb)
16. observer proper session hierarchy (according to build_graph): thus exported artifacts are always valid; (detail / hgweb)
17. tuned; (detail / hgweb)
18. clarified order: prefer bottom-up construction of partial content; (detail / hgweb)
19. more thorough update_global_index: overwrite old content; (detail / hgweb)
20. tuned; (detail / hgweb)
21. tuned; (detail / hgweb)
22. clarified HTML_Context: just one context type; (detail / hgweb)
23. unused (see also 217e6cf61453, 5e7916535860); (detail / hgweb)

Started by an SCM change

This run spent:

• 9.7 sec waiting;
• 1 hr 39 min build duration;
• 1 hr 39 min total from scheduled to completion.