tuned;

merged

proper 'no_syntax' declarations (amending 8e72f55295fd);

tuned, following make_symbs in src/Pure/Syntax/printer.ML;

clarified use of Lexicon.dummy; tuned signature;

unused (see 584828fa7a97);

tuned;

tuned;

tuned: prefer ML over prose;

eliminated redundant nt_count: rely on Symtab.size; tuned signature: more standard argument order;

eliminate unused prod_count (see also 7afca3218b65);

tuned;

more markup;

minor performance tuning: prefer static values;

tuned;

more markup;

clarified persistent datatype: more direct literal_markup, which also serves as a flag;

tuned signature;

clarified signature;

add comments to rendering, e.g. to collect them from build database;

To tiny but maybe useful lemmas (moved in from the AFP, Word_Lib)

tuned;

tuned;

tuned;

tuned;

tuned;

minor performance tuning for blocks without markup;

more markup <expression kind="item"> in Isabelle/Scala, with pro-forma Markup_Kind.setup in Isabelle/ML;

clarified signature;

tuned;

minor performance tuning: more direct blocks without markup; tuned signature;

tuned;

tuned signature;

proper 'no_syntax' (amending 8e72f55295fd);

more inner syntax markup: HOL;

misc tuning and clarification;

standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;

tuned;

minor performance tuning: more concise tuples;

tuned;

tuned;

tuned;

misc tuning and clarification;

more antiquotations;

tuned comments;

more specific markup for "judgment";

remove specific support for "expression" block markup: prefer "notation";

clarified inner syntax markup: use "notation" uniformly;

more uniform treatment of Markup.notation and Markup.expression: manage kinds via context;

clarified modules and signature;

proper fbreaks (amending 53f12ab896e6);

more inner syntax markup: minor object-logics;

more inner syntax markup: Pure;

more markup elements;

standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;

proper Haskell setup, following 406a85a25189;

support more markup elements;

block markup for specific notation, notably infix and binder; tuned;

clarified signature: more explicit operations;

tuned;

tuned;

no need to suppress positions (see ff3b8e4079bd) thanks to Context_Position.set_visible false (see 5328d67ec647);

tuned;

support for Markup.expression properties in pretty-blocks;

more positions; clarified defaults;

more operations;

more operations;

minor performance tuning: avoid vacuous update of context;

tuned;

proper Context_Position.report, following 5328d67ec647;

more operations;

more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory;

obsolete --- superseded by Local_Theory.syntax_cmd;

tuned;

unused (see 39261908e12f);

clarified signature; tuned comments;

tuned comments;

tuned;

more detailed markup;

more formal Markup.expression;

tuned;

clarified name space: no theory qualifier here --- treat like global datatype constructors;

discontinued "isabelle build -k": superseded by admin-tool "isabelle check_keywords";

clarified signature;

tuned signature;

obsolete (see also b93cc7d73431);

performance tuning: cache for highly redundant markup (types and sorts);

more operations;

tuned;

tuned;

tuned signature and module structure;

less ambitious Bytes.chunk_size for potentially more stable Poly/ML GC (see f0d8f659b19a, but also java.io.InputStream.DEFAULT_BUFFER_SIZE);

tuned signature: more operations;

clarified signature;

prefer Pretty.pure_string_of to produce output without markup, instead of cleaning output afterwards;

clarified signature: more explicit operations;

tuned: trim message before formatting;

tuned signature: more operations;

clarified signature;

clarified print_mode (again, amending 9de19e3a7231): support e.g. 'thm ("") symmetric' for formatting in ML and without markup;

more robust reports: ensure that markup is actually present;

tuned signature;

clarified internal tool output: prefer Pretty.pure_string_of over manipulation of print_mode;

unused;

misc tuning and clarification (see also 86a31308a8e1);

tuned signature: more operations;

clarified modules;

dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";

clarified YXML bootstrap;

tuned;

more robust: global ML name space for markup elements;

clarified properties;

clarified signature and modules;

further clarification of print_mode: PIDE markup depends on "isabelle_process" alone, Latex is stateless;

misc tuning and clarification;

minor performance tuning, notably for Bytes.add (e.g. YXML output);

revert 90f6e541e926, which has become pointless thanks to df85df6315af;

clarified signature and modules;

clarified files;

drop pointless print_mode operations Output.output / Output.escape;