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;