more robust display of bidirectional Unicode text: enforce left-to-right;

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;

reintroduced check that may guard some tactic failures

adapt theory names within the theory

made tactic more robust

tuned interface

merged

proper object-logic constraint (amending dd2914250ca7);

reconcile object-logic constraint vs. mixfix constraint;

more explicit support for object-logic constraint;

more language markup;

more accurate mixfix type constraints;

tuned;

tuned message;

more explicit type; tuned;

relevant check_mixfix happens further at the bottom, to avoid duplicate reports via Specification.prepare;

avoid duplicate reports;

tuned messages -- position is usually missing here;