Changes

Summary

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