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;

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;

lsp: added more triggerCharacters to make completion popups more consistent;

vscode: added default setting to make completions pop up by themselves;

lsp: improved completions;

vscode: removed unused code;

vscode: removed README because its content is outdated;

vscode: disabled whitespace rendering by default because the whitespace symbol is not monospace;

lsp: added symbol conversion request;

vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors;

vscode: removed unused import;

vscode: changed vscode_unicode_symbols_edits option default to true;

vscode: made uri equality check on actual strings, not on the functions;

vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent; disabled decoration requests as decoration caching is already done on client-side;

lsp: added rudimentary indenting to code actions;

vscode: adjusted setting description;

lsp: added support for code actions to apply active sendback markups;

lsp: clarified WorkspaceEdit;

lsp: made TextDocumentEdit accept optional versions;

lsp: tuned;

lsp: removed code that is never run;

lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;

clarified PIDE/line range conversions;

lsp: refactored conversion from Decoration_List to JSON;

lsp: tuned pretty_text_panel;

lsp: removed output_pretty_panel function as its logic is now in pretty_text_panel;

vscode: added more relevant options;

lsp: converted state panel to use a pretty text panel;

lsp: converted dynamic output to use a pretty text panel;

lsp: added Pretty_Text_Panel module;

vscode: added relevant isabelle options to vscode settings;

vscode: indent;

lsp: extracted panel content generation logic;

vscode: added all fonts to extension;

added vscode options tag;

vscode: tuned;

lsp: refactored non-html dynamic/state output;

vscode: reduced how often symbol width gets measured;

vscode: IsabelleDejaVuSansMono for state and output panel;

vscode: added decoration request on file switch;

lsp: added decoration_request notification;

lsp: added decorations to state updates;

lsp: added delay to dynamic_output updates after a set_margin;

lsp: added conversion of symbols for dynamic output so that decoration ranges consider vscode_unicode_symbols setting;

lsp: unified PIDE/decorations and dynamic output decorations format;

vscode: changed test_string to "mix" to be consistent with jEdit;

lsp: added decorations to dynamic output;

lsp: force update after state_set_margin;

vscode: added dynamic and state output set margin messages to vscode extension;

lsp: made margins synchronized;

lsp: added separation for non-html output and state;

lsp: tuned;

lsp: clarified preview_request;

lsp: added Symbols_Request;

lsp: added Output_Set_Margin and State_Set_Margin Notifications;

lsp: changed State_Init notification into a request and removed State_Init_Response;

lsp: tuned;

lsp: updated ErrorCodes;

lsp: added State and Dynamic Output html_output and margin handling;

lsp: added vscode_html_output option;

tuned formatting;

lsp: partially revert c0388fbd8096 to get decorations for all keywords;

lsp: added State_Init_Response message;

lsp: removed change_document normalization because it causes desyncs;

clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);

less markup: prefer "notatation" over "entity";

clarify comparison of output: ignore token positions, which are somewhat accidental;

clarified order of markup: more uniform input vs. output;

misc tuning;

clarified parse tree: always provide root node;

tuned signature;

tuned markup;

clarified markup: avoid conflict of "notation" with "entity", e.g. in "[x,y,z]" without spaces;

more flexible command syntax;

less markup (amending 07ad0b407d38): const = "" is mainly for parentheses syntax -- avoid entity_markup here;

more markup reports: notably "notation=..." within pretty blocks;

more parse tree positions;

more operations;

clarified order for 'print_syntax' command;

more accurate parse tree: retain all tokens (and thus positions);

more thorough markup reports (amending 0c6a600c8939 and 7f9e8516ca05): descend into vacuous nodes;

clarified comparison: prefer authentic nonterminal context, instead of somewhat accidental "const";

more detailed parse tree: retain nonterminal context as well;

clarified persistent data;

clarified input and output: support markup blocks via Bg/En; clarified datatype tree vs. tree_ops: reconstruct nested markup blocks via make_tree; clarified tree_ops_ord: ignore markup blocks, proceed like dict_ord;

tuned;

tuned;

more operations;

clarified output: count Tip entries;

tuned signature;

tuned whitespace;

clarified signature: more explicit type "output"; minor performance tuning of output_ord: static length;

clarified signature;

tuned: more uniform;

tuned: more uniform;

tuned;

minor performance tuning;

tuned;

tuned;

minor performance tuning;

partial revert of d97fdabd9e2b, to build old documentation more reliably;

tuned signature;

tuned signature;

tuned signature;

clarified signature;

minor performance tuning: proper table for parsetree list; tuned signature;

unused (see 954e9d6782ea);

tuned;

unused (see 7c1e73540990);

minor performance tuning (NB: order of prods / states does not matter);

tuned;

tuned;

tuned comments;

tuned;

pro-forma support for markup blocks, without any change of result yet;

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;

clarified signature: prefer explicit type Bytes.T;

clarified signature, roughly following Isabelle/Scala;

clarified print mode "latex": no longer impact Output/Markup/Pretty operations; renamed Output.output to Output.output_; removed Output.escape;

tuned comments, following Isabelle/ML;

tuned module structure;

tuned;

clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;

clarified signature;

tuned signature;

tuned;

minor performance tuning, following Isabelle/Scala;

tuned;

tuned signature;

more scalable;

tuned;

eliminate print mode "code_presentation" thanks to value-oriented Pretty.T operations;

NEWS: value-oriented Pretty.T;

proper formal sections;

tuned signature: more options;

clarified Pretty.markup_block: use value-oriented YXML.output_markup, with final re-interpretation via print_mode in output_tree; clarified Pretty.symbolic: always use YXML.output_markup;

minor performance tuning;

unused;

prefer static YXML.output_markup_only (without print_mode): Output.status is only relevant for PIDE (with print_mode "isabelle_process");

clarified signature: more explicit type output_ops: default via print_mode;

discontinued unused global variable (see also following bf465f335e85);

tuned signature;

clarified modules (see also ea7c2ee8a47a);

clarified signature: more explicit type "ops";

more thorough Protocol_Message.clean_output, following Isabelle/Scala;

more accurate output, following 3f02bc5a5a03;

clarified signature;

clarified signature;

misc tuning and clarification;

proper signature (amending 0f820da558f9);

more accurate output: observe depth as in "prune" operation;

clarified signature, following 1f718be3608b: Pretty.str is now value-oriented;

clarified signature and modules;

tuned;

clarified Pretty.T vs. output tree (following Isabelle/Scala): Output.output_width (via print_mode) happens during formatting, instead of construction; minor performance tuning: omit block_length for Pretty.symbolic and Pretty.unformatted;

clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;

clarified signature (see also 8bef51521f21);

tuned signature;

more accurate Default_Metric;

tuned signature;

clarified output_spaces, based on Output.output_width; tuned add_spaces;

clarified modules: enable pretty.ML to use XML/YXML more directly;

removed unused operation (reverting 4660b0409096);

clarified modules;

clarified signature;

tuned: prefer Symbol.spaces;

tuned whitespace;

tuned;

more NEWS;

proper string syntax (amending 70076ba563d2);

avoid redundant XML.blob: Bytes.contents consist of larger chunks;

minor performance tuning: avoid many small strings, notably in File_Stream.output;

A bit of tidying

merged

More tidying of old proofs

more scalable pretty printing: avoid exception String.Size at command "value" (line 33 of "$AFP/Iptables_Semantics/Examples/SQRL_Shorewall/Analyze_SQRL_Shorewall.thy") in AFP/c69af9cd3390;

more specific "args" syntax, to support more markup for syntax consts;

more direct notation;

more specific "args" syntax, to support more markup for syntax consts;

proper definition to avoid failure of HOL-Codegenerator_Test (amending 3d9e7746d9db);

further attempts at markup for monad notation;

more markup for syntax consts;

stop web server on close;

better results for terminated jobs;

more robust: clean up unfinished jobs on init, e.g. if build_manager process was forcefully terminated;

manage runner state properly (amending be4c1fbccfe8);

merged

More tidying of old proofs

more precise bound

merged

get rid of manual T_f defs

NEWS and documentation;

merged

use nicer notation, following 783406dd051e;

merged

A bit more tidying

more markup for syntax consts;

clarified Syntax.is_const (after 43c4817375bf): exclude logical consts from 'syntax_consts' / 'syntax_types', e.g. relevant for @{syntax_const} antiquotation;

use nicer notation, following 783406dd051e;

proper translation for "_qprod", following "_qsum" (see also e14b89d6ef13 and fa7d27ef7e59);

tuned: prefer notation for Pure.type;

tuned whitespace;

tuned;

tuned, following be8c0e039a5e;

more markup for syntax consts;

proper flags (amending 1319c729c65d): abbrevs are allowed, free variables are disallowed;

Some tidying

merged

Tidied some messy old proofs

merged

more markup for syntax consts;

more markup for syntax consts;

clarified concrete syntax;

more accurate markup (amending 43c4817375bf): only consider primitive syntax consts, avoid extra Markup.intensify e.g. due to "\<^const>Pure.all_binder";

more concrete syntax and more checks;

clarified signature: more operations;

support for syntax const dependencies, with minimal integrity checks;

tuned;

clarified markup: more uniform treatment of parse/print phase;

tuned;

clarified markup: more uniform;

tuned signature: separate markup vs. extern;

clarified signature;

tuned: prefer configuration options via context;

tuned;

tuned signature: more operations;

tuned comments

merged

Partial tidying of old proofs

merged

new version of time_fun that works for classes; define T_length automatically now

merged

revised/generalised some lemmas

remove terminated jobs, even if futures do not complete;

terminate jobs properly;

clarified signature: eliminate clones;

tuned: more antiquotations;

tuned: more antiquotations;

misc tuning;

tuned: eliminate clone (with change of internal exceptions);

tuned: more antiquotations;

tuned comments and whitespace (see also 589645894305);

tuned: more antiquotations;

tuned: more antiquotations;

proper const (see also 759bffe1d416 and b2800da9eb8a);

tuned: inline constants;

tuned: eliminate clone;

tuned: more antiquotations;

prefer host that is less likely to be down;

adapt and activate congprocs examples, following the current Simplifier implementation; minor tuning;

original Congproc_Ex.thy by Norbert Schirmer: still inactive;

provide Simplifier.set_mksimps_context (roughly following Norbert Schirmer): allow update of context when premises are added to the local simpset;

clarified signature;

more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;

tuned;

support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;

tuned;

tuned: anticipate congprocs;

clarified signature;

tuned signature (again): anticipate different kinds of procs;

clarified context data; tuned: more antiquotations;

tuned: prefer canonical argument order;

tuned: more antiquotations;

tuned: prefer canonical argument order;

clarified signature: less redundant types;

clarified signature;

unused (see d12c58e12c51);

tuned signature: support more general procedures;

merged

tuned: more antiquotations;

tuned;

tuned: more antiquotations;

tuned whitespace;

more robust (amending 8f53fa93d5f0): R could be anything and Thm.instantiate' involves some type-checks, e.g. relevant for lemma fset_simps in theory Quotient_Examples.Quotient_FSet;

tuned modules;

misc tuning;

tuned;

tuned: more antiquotations;

misc tuning;

misc tuning and clarification;

tuned;

misc tuning and clarification: proper context, proper exception;

tuned: eliminate odd clones;

tuned: more antiquotations;

unused;

tuned: more antiquotations;

tuned: more antiquotations;

tuned: more antiquotations;

tuned proofs;

tuned signature: more operations;

tuned;

tuned: more antiquotations;

clarified signature;

Two little lemmas

merged

more uniform Type_Infer_Context.infer_types_finished, despite subtle differences of Type_Infer.fixate vs. Proof_Context.standard_term_check_finish;

tuned, following cdae621613da;

tuned;