Summary
- merged
- merged
- explicit warning about bidi uncertainty in Unicode;
- explicit warning about formal use of Unicode;
- documentation;
- more markup;
- require actual space;
- tuned signature;
- required space is already part of Position.here;
- tuned messages;
- clarified errors -- disallow cartouche fragments as delimiter;
- tuned signature;
- tuned;
- clarified end position;
- tuned signature;
- tuned;
- removed redundant Position.set_range -- already done in Position.range;
- lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
- less bulky timing information, e.g. HOL 56913 ~> 672;
- tuned;
- more operations (cf. Scala version);
- tuned whitespace;
- explicit property for unbreakable block;
- unused;
- tuned markup;
- clarified treatment of properties; tuned messages;
- more robust pretty printing: permissive treatment of bad values;
- adapted to Poly/ML repository version 2e40cadc975a;
- explicit mixfix block properties;
- clarified modules;
- tuned signature;