Changes

Summary

1. merged;
2. more robust GUI initialization (amending 29441f2bfe81);
3. clarified signature: just one common operation;
4. clarified paths and links; proper node_context for aux. files: to get links within them;
5. more concise output of files: just one round;
6. more robust;
7. proper node_dir within presentation_dir, not source file directory;
8. clarified modules;
9. clarified names;
10. more thorough checks of browser_info file conflicts;
11. tuned;
12. prefer strict operations with explicit errors (instead of missing HTML output);
13. more thorough check, without path name artifacts (e.g. "./README");
14. tuned signature; tuned messages;
15. clarified signature: Sessions.Base_Info follows Sessions.Base;
16. clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
17. tuned;
18. tuned whitespace;
19. evade clash with index.html (allow "Index.thy" even on case-insensitive file-systems);
20. discontinued special support for README.html (which was hardly ever used in the past 2 decades);
21. clarified directory layout (again): mimic original directory layout, notably ISABELLE_HOME;
22. more robust treatment of Document.Node.Name, following stored data;
23. more robust;
24. clarified directory layout: files are relative to enclosing theory;
25. tuned signature: avoid duplication;
26. more robust: theories could have been suppressed via option "condition";
27. tuned signature;
28. tuned messages (again, see d50c2129e73a): presentation setup could fail initially for take some time;
29. clarified modules;
30. clarified signature: support for adhoc file types;
31. clarified Presentation.Nodes, with explicit Nodes.Session and Nodes.Theory; distinguish Nodes.Theory.static_session vs. dynamic_session: refer to exports from dynamic_session, corresponding to strictly to build_graph; more robust treatment of source files and links to generated files; retrieve entities by their file position, within its corresponding session/theory hierarchy;
32. export entity file position as well, e.g. relevant for HTML presentation with aux. files;
33. proper permissive = true (amending 475fedc02737)
34. tuned signature;
35. clarified signature;
36. clarified signature;
37. more robust directory structure: always relative to session_dir; tuned messages;
38. discontinued slightly odd integrity check (from af2d0e07493b): requires a different approach;
39. clarified signature;
40. misc tuning and clarification;
41. unused;
42. tuned signature;
43. tuned signature;
44. tuned signature;
45. clarified modules;
46. clarified modules;
47. unused;
48. tuned signature;
49. clarified signature: replaced Sessions.Deps by Sessions.Structure from HTML_Context;
50. tuned;
51. clarified signature: avoid constants from Sessions.Structure within Session.Base;
52. clarified signature: avoid object-oriented HTML_Context; clarified theory_qualifier --- belongs to the overall Sessions.Structure;
53. tuned type signature
54. tuned type signature
55. streamlined theorems
56. more thorough split rules for div and mod on numerals, tuned split rules setup
57. streamlined simpset building, avoiding duplicated rewrite rules
58. consolidated attribute name
59. streamlined theorems
60. streamlined theorems and sections