Changes

Summary

1. merged
2. tuned;
3. tuned signature;
4. clarified database content;
5. more operations;
6. optional ml_statistics: much faster;
7. proper query (amending ce15da15f8e2);
8. put bulky data last;
9. tuned;
10. more log files;
11. clarified multi-line properties;
12. dummy session entry for empty build_info: relevant for filter_files;
13. tuned query, notably for isabelle_build_log_build_info;
14. operations to read database;
15. tuned signature: less overloading;
16. tuned signature;
17. tuned transaction granularity;
18. unused;
19. clarified database layout;
20. tuned signature: avoid null in regular Scala code;
21. clarified transaction boundaries: more robust incremental write operations;
22. clarified database layout;
23. allow null for primitive types;
24. more uniform storage of Meta_Info;
25. allow null;
26. clarified plain_name / log_name;
27. tuned comment;
28. tuned signature;
29. tuned;
30. separate small meta_info vs. big build_info;
31. tuned;
32. unused;
33. tuned signature;
34. more standard multi-line storage in database: Prop.separator is only required for single-line meta_info within log file;
35. clarified filter_files: sorted and unique;
36. database storage of Meta_Info and Build_Info;
37. allow null;
38. more encode/decode operations;
39. proper prefix;
40. support for database connection;
41. clarified treatment of default port;
42. tuned signature;
43. clarified modules;
44. more SQL operations;
45. more robust (see also 6688b9cd443b);
46. more robust treatment of non-UTF8 text files (cf. 3ed43cfc8b14), notably old log files in ISO-8859-15;
47. clarified signature;