more syntax bundles;

clarified bundles for list syntax;

more robust declarations via "no syntax" bundles;

more accurate no_syntax declarations, following ec121999a9cb;

more robust syntax; tuned proofs; drop unused ML snippet;

avoid syntax clashes;

tuned whitespace, to simplify hypersearch;

avoid syntax clashes;

clarified mixfix annotations;

more inner-syntax markup; more syntax bundles for use with "unbundle no foobar_syntax";

more inner-syntax markup, without pretty blocks;

tuned output;

tuned comments: all times are < 1ms;

support for pretty blocks that are "open" and thus have no impact on formatting, only on markup; effectively revert 2cb4a2970941 and unify pretty-printing in Scala and ML, following Scala before that change; build error messages are properly formatted again (amending 320bcbf34849): "no_report" markup does not affect its enclosed line break anymore;

clarified signature;

tuned;

more inner-syntax markup;

ML antiquotation for formally-checked bundle names;

first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;

misc tuning;

documentation for pretty block "notation" markup;

clarified syntax for opening bundles; updated and tuned documentation;

tuned;

clarified bundles for syntax modifications;

bundles for syntax modifications seen in AFP;

tuned;

merged

more standard bundle names;