Changes

Summary

1. merged
2. merged
3. explicit warning about bidi uncertainty in Unicode;
4. explicit warning about formal use of Unicode;
5. documentation;
6. more markup;
7. require actual space;
8. tuned signature;
9. required space is already part of Position.here;
10. tuned messages;
11. clarified errors -- disallow cartouche fragments as delimiter;
12. tuned signature;
13. tuned;
14. clarified end position;
15. tuned signature;
16. tuned;
17. removed redundant Position.set_range -- already done in Position.range;
18. lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
19. less bulky timing information, e.g. HOL 56913 ~> 672;
20. tuned;
21. more operations (cf. Scala version);
22. tuned whitespace;
23. explicit property for unbreakable block;
24. unused;
25. tuned markup;
26. clarified treatment of properties; tuned messages;
27. more robust pretty printing: permissive treatment of bad values;
28. adapted to Poly/ML repository version 2e40cadc975a;
29. explicit mixfix block properties;
30. clarified modules;
31. tuned signature;