tuned message;

Added Circle_Area to HOL-Analysis examples

tuned/minimized

added lemma

tuned whitespace;

more robust: delay switches thread context from timer to GUI and may get out of sync with revoke operation;

tuned signature;

tuned signature;

improved chart plotting

augmented user aliasses

proper treatment of utf-8

tuned;

support for semantic completion;

generalized types in lemmas

updated package;

enable vscode_unicode_symbols by default, despite asymmetry of input and output;

more documentation;

generated configuration for Prettify Symbols Mode;

tuned;

clarified text output wrt. symbols;

merged

tuned signature;

support "purge" operation on document model;

proper template;

tuned;

accomodate very big file_models and changed_files;

tuned;

tuned

separate instance for semidom_modulo

generalized definition

tuned output;

update File_Model based on file-system events;

tuned;

clarified modules; tuned;

tuned;

tuned signature;

merged

fix problems because of "surj" input abbreviation; tuned

hide global sum

gcd/lcm on finite sets

moved some lemmas to appropriate places

slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization

fixed LaTeX problems

Jordan Curve Theorem

Advanced topology

NEWS for VSCode;

merged

more documentation;

added node_name(String): imitate jEdit buffer operations; more uniform get_file_content for external source file references;

tuned;

tuned signature;

avoid immediate editor.flush on buffer events;

refer to internal File_Model instead of external file;

tuned;

resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;

tuned;

support for bibtex entries;

tuned;

tuned signature;

more explocit Document_Model.Content;

refer to bibtex entries via general Document_Model, instead of editor buffers;

clarified modules;

uniform Document.Model.node_edits (without void edits);

clarified check_thy_reader: check node_name here;

more uniform node_header (non-strict); removed dead code;

tuned signature;

tuned signature;

tuned;

clarified lazy text content;

Line.Document consists of independently allocated strings; tuned signature;

obsolete;

clarified buffer events: exit model while loading; misc tuning;

separate Buffer_Model vs. File_Model; misc tuning and clarification;

tuned;

tuned;

tuned;

manage buffer models as explicit global state; tuned signature;

tuned signature;

obsolete

more informative error for spurious crash;

merged

tuned;

dummy File_Watcher for Windows (spurious crashes seen on Windows 7);

more robust treatment of logical lines;

updated package;

proper name for recursive grammar; pro-forma update of fileTypes;

emit Commands_Changed for blobs as well, e.g. relevant for isabelle.vscode.Server.prover_output;

suppress empty results;

tuned;

manage document blobs as well;

misc tuning and clarification;

tuned;

tuned;

tuned;

tuned structure

lead_coeff is more appropriate as abbreviation

more lemmas; tuned headings

covering space lift lemmas

facts about ANRs, ENRs, covering spaces

New theory of arcwise connected sets and other new material

connectedness, circles not simply connected , punctured universe

New material about path connectedness, etc.

tuned NEWS

reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings

moved euclidean ring to HOL

reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion

proper registration of implicitly loaded files;

tuned;

merged

more file types;

tuned;

proper interpretation of Resources.source_file as platform file;

clarified Document.Node.Name (again): canonical platform file; identify document models by native java.io.File;

Windows UNC path is plain file;

clarified file URIs;

Merge

Many new theorems, and more tidying

merged

tuned

more robust, notably on Windows;