Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

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

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

1. merged
2. more complete theorem_commands;
3. clarified signature, following Isabelle/b6d74c90b588;