Changes

Summary

1. merged
2. clarified execution context: main work happens within Future.thread; clarified signature: only one "join" operation;
3. clarified timeout: closer to actual process;
4. tuned names;
5. clarified names;
6. tuned, following ML_Statistics.monitor;
7. unused (see also 0cebcbeac4c7);
8. tuned;
9. tuned;
10. tuned comments;
11. clarified modules; tuned signature; tuned comments;
12. clarified modules;
13. clarified modules;
14. clarified signature;
15. clarified modules;
16. clarified modules;
17. tuned;
18. clarified modules;
19. clarified modules;
20. tuned;
21. more robust: proper synchronization of transition from next_job to start_session;
22. more thorough synchronized_database for internal *and* external state;
23. simplified startup under "locked" condition (in contrast to f7e413e8d269);
24. more explicit session name, in anticipation of variants like "session.document", "session.browser_info";
25. tuned signature;
26. tuned signature;
27. tuned signature;
28. tuned signature: support general Build_Job instances;
29. tuned signature;
30. clarified signature: prefer static data;
31. tuned signature;
32. identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
33. tuned signature;
34. tuned signature;
35. tuned signature;
36. tuned;
37. unused;
38. tuned signature (again);
39. tuned;
40. tuned;
41. proper deps from build_graph, not imports_graph (amending 0c704aba71e3);
42. misc tuning: more direct access to ancestors, without build_graph;
43. tuned signature (again);
44. clarified signature: reduce explicit access to static Sessions.Structure;
45. tuned signature;
46. clarified modules (again);
47. tuned;
48. tuned signature;
49. avoid premature Properties.uncompress: allow blob to be stored in another database;
50. more robust: synchronized access to database;
51. clarified signature: do not expose global state to object-oriented variants;
52. tuned comments and outline;
53. merged
54. Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed
55. A little bit more tidying up