Changes

Summary

1. merged
2. NEWS;
3. support XZ compression in Isabelle/ML;
4. prefer scalable byte strings;
5. more scalable byte messages, notably for Scala functions in ML;
6. tuned comments;
7. clarified ML pretty printing;
8. clarified signature: more operations;
9. tuned signature;
10. tuned comments;
11. tuned signature: more operations;
12. tuned signature: more operations;
13. tuned signature;
14. clarified signature: avoid repeated string copying via Substring.slice;
15. support for scalable byte strings, with incremental construction;
16. clarified signature;
17. remove unused file following 51e696887b81;