clarified options; tuned messages;

Some new library lemmas

merged

really removing Dedekind_real

merged

Moving Dedekind_Real to the AFP

tuned

separated case reduction

separated selector function entirely

self-contained extraction auf clauses

extracted selector function, restoring code generation for let expressions

streamlined

streamlined

streamlined

disentangled

merged

tuned message;

more operations;

tuned signature;

more robust install/uninstall; clarified extension_name (again): --locate-extension wants to see a lowercase name;

more formal extension_manifest, with shasum for sources;

tuned;

tuned signature;

clarified signature;

proper usage;

tuned -- follow sha1_digest in src/Tools/Setup/src/Build.java;

tuned signature;

clarified modules;

tuned signature;

... and removing Primrec from ROOT too

Removal of the Primrec example in preparation for making it an AFP entry

merged

avoided recomputation in Cooper.djf and ran `isabelle regenerate_cooper`

split veriT reconstruction into Lethe and veriT part

clarified options;

more robust errors -- on foreground process instead of background server;

clarified options -l vs. -R;

command-line arguments for "isabelle vscode", similar to "isabelle jedit";

proper command-line tool;

support console output, e.g. "isabelle vscode -C -- --help";

run Isabelle/VSCode via Scala;

clarified module name;

clean build from explicit MANIFEST: avoid accidental garbage in vsix package;

incorporate build_grammar into build_vscode_extension;

removed old generated file;

Tidied several ugly proofs in some elderly examples

tuned message;

clarified errors;

tuned messages;

support Node.js as well, reusing the engine from Electron/VSCodium;

updated to vscode 1.65.2;

proper result check;

merged

clarified directory layout and settings: more robust on all platforms;

tuned;

support Electron application framework; clarified vscodium startup;

generated lemma map_ident_strong for BNFs

updated SMT certificates

used more descriptive assert names in SMT-Lib output

clarified and unified executable names;

tuned;

tuned;

merged

suppress OCaml icons: avoid conflict of .ml and .ML, due to case-insensitive file-names in VSCode;

fix handling of lambdas in reconstruction of eq_congruent

more robust: avoid breakdown of Search dialog;

tuned;

always use Isabelle encoding, as in Isabelle/jEdit;

tuned signature;

clarified signature: more uniform ts vs. Scala;

discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249; discontinued special treatment of workspace_dir as session directory;

actually decode/encode symbols;

merged

prefer yarn over npm;

more accurate .hgignore;

clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode;

tuned messages;

proper init_resources for macos;

clarified names;

clarified modules: vscode vs. extension; clarified signature;

inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs;

more operations;

tuned comments; tuned messages;

patch VSCode source tree to support isabelle_encoding.ts;

more robust, pass "yarn valid-layers-check";

clarified directories;

patch for vscode encoding "UTF-8-Isabelle": clone of "utf8", no symbols yet;

fit into vscode source conventions;

A tiny further cleanup

Tidied some messy proofs

merged

more count_list lemmas

towards UTF-8-Isabelle symbol encoding;

updated to VSCode 1.65.0;

clarified char symbols: cover most European languages;

more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML);