Changes

Summary

1. modernized, reordered, generalized
2. more correct type annotation
3. proper build with jdk-21 (amending 4fb5e6499da9);
4. NEWS;
5. update to jdk-21.0.1; enforce rebuild of Isabelle/Scala + Isabelle/ML;
6. rebuild jedit with minimal patch for jdk-21, following SVN 25690;
7. clarified modules;
8. suppress duplicate entries systematically using log_name: e.g. relevant for AFP;
9. clarified operation: pick current pull_date instead of previous one;
10. operations AND, OR, XOR are specified by characteristic recursive equation
11. clarified toml keys operations;
12. tuned;
13. clarified toml keys: more operations;
14. use toml key operations properly; clarified module;
15. clarified toml keys formatting vs. toString;
16. clarified keys module;
17. pull out toml keys module;
18. clarified toml parser interface;
19. prefer symbolic build_history_base_arm;
20. build_history: proper support for ISABELLE_APPLE_PLATFORM64;
21. clarified isabelle_hg (again, see b9d59669904a);
22. clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
23. clarified signature: more operations and options concerning Isabelle hg;
24. performance tuning: cache graph;
25. tuned signature: fewer warnings in IntelliJ IDEA;
26. unused (see also 004b39bf06a5);
27. clarified signature and modules: more explicit Build_Log.History;
28. tuned: avoid recursion;
29. tuned;
30. avoid duplicate data;
31. output more data;
32. tuned whitespace;
33. clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
34. proper ml_statistics (amending aeb511a520f4);
35. unify error messages;
36. add file information to toml parse context and error messages;
37. add position information to toml parser and error messages;
38. properly concatenate toml files: regular toml rules still apply (e.g., inline values may not be changed), but values defined in one file may be updated in another;
39. allow re-defining keys in toml object (already checked during parse time);
40. clarified toString for toml objects;