Changes

Summary

1. backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;
2. enforce rebuild of Isabelle/ML + Isabelle/Scala;
3. updated to jdk-17.0.7;
4. minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
5. performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%;
6. more operations;
7. tuned: more readable ML;
8. tuned;
9. backed out changeset 4660181c83c9: remove rather pointless timing (1..50ms);
10. maintain dynamic position where values are created (again, amending afa6117bace4);
11. more robust: publish token only after assignment of result;
12. tuned comments;
13. clarified signature;
14. merged
15. tuned signature;
16. support for cached evaluation via weak_ref;
17. optional timing;
18. more informative trace of context allocations;
19. tuned;
20. tuned internal structure;
21. tuned;
22. tuned whitespace;