clarified inner-syntax markup;

more syntax bundles;

more NEWS;

more inner-syntax markup;

back to specific nonterminals (amending 52ed95fa4656): otherwise AFP/CakeML won't terminate;

uniform \<Sum> and \<Prod> syntax, following d10fafeb93c0;

more NEWS;

more accurate datatype_record_syntax;

more syntax bundles, less clones;

more syntax bundles;

more syntax bundles;

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;

provide 'open_bundle' command;

tuned module structure;

tuned;

more inner syntax markup;

more syntax: avoid duplication in AFP;

clarified abbreviation;

tuned whitespace;

tuned;

more NEWS;

more inner syntax markup: HOL-Analysis;

tuned markup;

more inner syntax markup: HOLCF;

more 'no_syntax' bundles;

more robust 'no_syntax' via bundles;

tuned markup;

drop somewhat pointless 'syntax_consts' declarations;

clarified syntax: use outer block (with indent);

clarified syntax: prefer nonterminal "args", use outer block (with indent);

proper command kinds;

updated vscode_extension;

NEWS and CONTRIBUTORS;

clarified: add operation;

minor tuning;

lsp: added additional commit characters to immediate completions;

vscode: further adjusted default settings and wordPattern for consistent completion popups; for some reason wordPattern must be set to match (almost) everything, otherwise completions only pop up every other character, and then we must disable wordBasedSuggestions or it will suggest whole lines out of the document;