clarified signature;

tuned: fewer warnings in IntelliJ IDEA;

clarified signature;

clarified modules: more re-usable;

proper protocol messages (amending 7a1f9e571046);

clarified treatment of caret_range: better support for multiple (unrelated) selections;

tuned whitespace;

support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;

clarified rendering: entity acts as atomic notation / expression;

more rendering for Markup.COMMAND_SPAN, following Rendering.structure_elements;

more NEWS;

merged

support Isabelle/jEdit action isabelle.select_structure; update component jedit-20241101;

more operations;

clarified text;

update to jedit5.7.0;

GUI option "editor_auto_hovering" for Output panel;

update to scala-3.3.4 LTS;

removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;

Library material from Eberl's Parallel_Shear_Sort

Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult

use automatically generated time function in HOL-Data_Structures.Selection

merged

better time_functions (let)

less hidden configuration;

proper passwordless smtp check: must be null;

adjusted documentation

more attribute tuning

tuned attributes

merged

added lemmas

tuned proofs;

tuned NEWS;

markup for "..." notation; clarified signature;

more robust: avoid non-authentic translations;

tuned whitespace of sources;

update documentation; tuned typesetting;

tuned;

update documentation: print mode "latex" only affects syntax tables, but output of symbols;

misc tuning and clarification;

clarified section structure;

tuned;

tuned;

tuned;

tuned signature;

clarified symbolic output: avoid redundant "block" element for open_block = true;

clarified signature;

clarified (again): Markup.intensify is already part of Variable.markup_fixed for undeclared variable, Markup.fixed is already part of Mariable.markup;

more accurate Symbol.length;

tuned;

merged

more inner-syntax markup;

obsolete (see a8502d492dde);

minor performance tuning;

tuned proofs; tuned whitespace;

more inner-syntax markup;

merged

time_fun: lambdas and lets work now

variable instantiation in Sledgehammer and Metis

prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);

revert b35c2aa05fcf: redundant due to 89ea66c2045b, if object-logic judgment lacks delimiters;

clarified position constraints: omit redundant information, e.g. for implicit object-logic judgment;

unused (see 0199acc01aa8);

tuned;

more robust: avoid ambiguity of contract_abbrevs;

misc tuning: more concise (or hermetic) pointfree style;

provide rewrite_term_yoyo, which is analogous to Ast.normalize;

tuned signature;

tuned names; tuned whitespace;

tuned;

misc tuning and clarification;

tuned;

misc tuning and clarification;

merged

adhoc option to disable const constraints, notably for AFP/Isabelle_DOF;

unused;

tuned signature;

proper treatment of position constraints;

more liberal ast matching, notably for case-translations in HOLCF that operate on logical consts rather than syntax consts;

more parser markup, based on position constraints for logical mixfix syntax;

more concise representation of term positions;

more robust;

tuned signature;

tuned comments;

misc tuning and clarification;

clarified concrete vs. abstract syntax: avoid translations on logical consts;

misc tuning and clarification;

clarified markers for syntax consts: avoid overlap with logical consts;

update ci mail address;

minor performance tuning;

notable performance tuning (amending a59d9b81be24 and 8976c5bc9e97): avoid costly could_beta_eta_contract, which traverses the whole term; always use Item_Net.retrieve instead, but on frozen TVars/Vars to enforce matching instead of unification;

tuned;

clarified signature;

tuned whitespace;

support multiple positions (non-empty list);

more robust syntax translation;

clarified concrete vs. abstract syntax;

more inner-syntax markup;

clarified concrete vs. abstract syntax;

clarified concrete vs. abstract syntax;

more operations;

tuned;

tuned signature;

more operations;

more accurate treatment of constraints: restrict permissive mode to output;

tuned;

tuned proofs;

clarified order of tooltips: make it less dependent on report order from ML (which differs for input vs. output);

clarified signature (see also 1de8a8b1ae79);

clarified signature;

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;

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;