replaced recdef by fun

spelling

merged

added spell-checker completion;

clarified modules;

tuned;

clarified modules;

tuned signature; clarified modules;

clarified modules;

tuned;

clarified signature;

Repaired an inadvertent reordering of the premises of two theorems

New theorems; stronger theorems; tidier theorems. Also some renaming

merged

adapted to new simp lemmas

added simp rules

more permissive: avoid situations where query is silently ignored;

more robust: do not touch unrelated directory isabelle_repos_other (i.e. bad argument);

always start with fresh clone (with explicitly given rev): more robust on Windows;

reverted 94cad7590015: does not help much on Windows;

tuned signature;

merged

updated package;

maintain overlays within main state of document models; proper pending_input for Isabelle/VSCode;

proper treatment of editor overlays;

tuned;

clarified modules;

tuned signature;

support for separate proof state output;

automatic reformatting;

more general dispatcher operations;

tuned;

clarified modules;

tuned;

tuned;

Some new material. SIMPRULE STATUS for sum/prod.delta rules!

tuned

simplified delete/proof

clarified signature;

added abstract editor operations, notably for Query_Operation;

tuned signature;

tuned;

clarified modules;

clarified modules;

updated package;

tuned GUI;

obsolete;

removed pointless entries: not part of api.LanguageEntry;

avoid overlapping line background, notably for "quoted";

tuned rendering;

tuned;

clarified message;

retain vacuous CompletionProvider for now;

tuned;

dynamic configuration of prettify-symbols-mode, similar to VSCoq;

obsolete;

removed pointless default: vscode.previewHtml happens only after prover response;

more markup for HTML rendering;

tuned signature;

clarified;

tuned;

superseded by external protocol;

use old-style "textEdit" for the sake of the external protocol (see also vscode-languageserver-node/issues/188);

tuned;

symbol completion that bypasses the LS protocol, and thus observes the range properly; more symbol operations;

More rules for Probability/Tree_Space

merged

tuned;

clarified output for symbol completion;

tuned;

more uniform syntax_completion + semantic_completion;

clarified modules;

provide information about Isabelle symbols within VSCode;

tuned signature;

Cleaned up and extended Probability/Tree_Space

HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections

avoid markup, for the sake of Build_Log.Log_File.parse_props;

more robust: store important meta info before potential failure;

tuned message;

merged

more HTML rendering as in Isabelle/jEdit; tuned;

tuned signature;

clarified menu; avoid non-portable ALT-mouse combination;

clarified signature;

HTML preview based on PIDE markup;

explicit foreground color, for the sake of dark theme in VSCode;

tuned layout (amending 8040d2563593);

more official session qualifier;

clarified;

replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace

merged

clarified output;

more tooltips;

clarified imports;

update strictly local imports only;

proper imports_base;

tuned;

avoid redundant Preview documents;

HOL-Probability: add measurable space for trees

clarified import of loaded theory;

decomposed tuple

tuned

clarified message

tuned signature;

discontinued obsolete print mode;

HTML preview via builtin HTTP server;

permissive output of XML.Text, e.g. relevant for embedded <style>;

avoid Local_Theory.reset in application space

tuned

specific output setup is not supposed to intrude regular import theory

avoid duplicate

streamlined code setup for fake terms

modernized (code) setup for enumeration predicates

simplified setup

executable domain membership checks

more tests;

cover more history;

cover more history;

uniform notion of Symbol.is_controllable (see also 265d9300d523);

merged