#1743 (Aug 8, 2022, 12:50:06 AM)

1. tuned message; (detail / hgweb)
2. afford default cache policy, despite 6a29709906c6; (detail / hgweb)
3. tuned signature; (detail / hgweb)
4. clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory; (detail / hgweb)
5. tuned; (detail / hgweb)
6. tuned signature; (detail / hgweb)
7. clarified signature; (detail / hgweb)
8. clarified modules; (detail / hgweb)
9. merged (detail / hgweb)
10. tuned; (detail / hgweb)
11. clarified message; (detail / hgweb)
12. clarified signature: prefer Export.Session_Context over Sessions.Database_Context;
    discontinued obsolete operations; (detail / hgweb)
13. clarified signature: prefer Export.Context; (detail / hgweb)
14. clarified signature: find session_database within Session_Context.db_hierarchy; (detail / hgweb)
15. clarified signature: prefer Export.Session_Context; (detail / hgweb)
16. prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context; (detail / hgweb)
17. clarified signature; (detail / hgweb)
18. tuned signature, following hints by IntelliJ IDEA; (detail / hgweb)
19. clarified signature: more robust treatment of server; (detail / hgweb)
20. discontinued Export.Provider in favour of Export.Context and its derivatives;
    uniform treatment of all sessions, including Pure; (detail / hgweb)
21. clarified signature: less redundant -- Sessions.Base_Info already specifies the main session; (detail / hgweb)
22. tuned signature: more operations; (detail / hgweb)
23. misc tuning and clarification; (detail / hgweb)
24. clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
    clarified treatment of Session_Context.theory_names, added export_names;
    clarified treatment of document_snapshot: sites on top of the session_stack; (detail / hgweb)
25. clarified database query: refer to semantic theories; (detail / hgweb)
26. clarified signature: more operations; (detail / hgweb)
27. clarified signature: persistent theory_names in lexical order; (detail / hgweb)
28. proper session_databases for database_server: need to follow precise session_hierarchy; (detail / hgweb)
29. redundant; (detail / hgweb)
30. clarified signature: more robust close operation; (detail / hgweb)
31. more uniform exports: proper encoding of empty parents for Pure; (detail / hgweb)
32. clarified signature: more uniform treatment of empty exports; (detail / hgweb)
33. clarified session name: treat PIDE session as Sessions.DRAFT with imports from other sessions; (detail / hgweb)
34. more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
    removed unused imports_hierarchy; (detail / hgweb)
35. clarified context for retrieval: more explicit types, with optional close() operation; (detail / hgweb)
36. tuned; (detail / hgweb)
37. unused; (detail / hgweb)
38. retrieve information about used files; (detail / hgweb)
39. tuned signature -- more robust; (detail / hgweb)
40. tuned signature; (detail / hgweb)
41. clarified signature: Export.Provider knows its (accidental) theory_names; (detail / hgweb)
42. clarified signature; (detail / hgweb)
43. tuned, following hints by IntelliJ IDEA; (detail / hgweb)
44. clarified signature: proper session_name for Sessions.Base (like Sessions.Info); (detail / hgweb)
45. tuned signature; (detail / hgweb)
46. clarified signature; (detail / hgweb)
47. clarified signature; (detail / hgweb)
48. clarified signature; (detail / hgweb)
49. avoid multiple load_commands; (detail / hgweb)
50. avoid redundant dependencies.load_commands with potential errors (amending ea4f86914cb2); (detail / hgweb)
51. tuned signature -- avoid redundant arguments; (detail / hgweb)
52. tuned -- following hints by IntelliJ IDEA; (detail / hgweb)
53. tuned signature; (detail / hgweb)
54. tuned comments; (detail / hgweb)
55. removed somewhat pointless transaction: db is meant to be finished (or updated monotonically); (detail / hgweb)
56. tuned signature; (detail / hgweb)
57. clarified signature; (detail / hgweb)
58. clarified signature: avoid repeated db_context.input_database; (detail / hgweb)
59. clarified signature: more robust; (detail / hgweb)
60. removed somewhat pointless operations (see a6c69599ab99); (detail / hgweb)
61. clarified signature; (detail / hgweb)
62. tuned; (detail / hgweb)
63. tuned; (detail / hgweb)
64. clarified signature; (detail / hgweb)
65. clarified names; (detail / hgweb)
66. clarified signature; (detail / hgweb)
67. clarified names; (detail / hgweb)
68. clarified signature; (detail / hgweb)
69. clarified signature: more explicit types; (detail / hgweb)
70. unused (see 0d30ea76756c); (detail / hgweb)
71. tuned; (detail / hgweb)
72. clarified signature; (detail / hgweb)
73. tuned; (detail / hgweb)
74. unused (see 3064e165c660); (detail / hgweb)

Started by an SCM change

This run spent:

• 5.6 sec waiting;
• 1 hr 47 min build duration;
• 1 hr 48 min total from scheduled to completion.