Changes

Summary

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