more type information; clarified signature;

more type information;

clarified signature;

clarified signature;

tuned signature;

clarified signature;

suppress dummyT, e.g. from Type_Annotation.print;

tuned proofs;

print type constraints for consts with mixfix syntax;

tuned comments;

obsolete (see 137ea3d464be);

tuned proofs;

tuned whitespace;

more inner-syntax markup;

less instrusive rendering for input buffer (in contrast to 264f043c5da1);

clarified inner-syntax markup;

tuned whitespace;

tuned whitespace;

clarified syntax declarations: keep things together;

tuned;

more inner-syntax markup;

tuned proofs;

more ambitious rendering: highlight active area for mouse hovering without modifier;

tuned proofs;

show_consts_markup is enabled by default;

clarified signature (again, reverting ec1023a5c54c);

clarified signature: more explicit Syntax.print_mode_tabs, depending on print_mode_value (); tuned data structures;

redundant;

tuned signature;

performance tuning: cache markup and extern operations;

minor performance tuning;

minor performance tuning;

backout somewhat pointless 5ea48342e0ae: no need to declare syntax consts for translations (e.g. constraints);

tuned;

tuned;

revert redundant guard (T = dummyT) from 0278f6d87bad;

allow type constraints for const_syntax; cope with that in ast translations and mixfix templates; minor adjustments to print_ast_translation functions in ML;

tuned;

tuned;

tuned;

tuned;

tuned;

merged

misc tuning and clarification;

tuned;

tuned: more readable names;

tuned;

tuned;

misc tuning and clarification; more accurate scope of "handle Match";

clarified signature;

clarified signature; tuned comments;

misc tuning and clarification;

eliminate clones: just one Collect_binder_tr';

clarified signature;

tuned;

new HO time functions

tuned NEWS;

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;