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;

updated package;

merged

support VSCode DocumentHighlights; clarified modules;

clarified file URLs, notably for Windows UNC paths;

more language support;

tuned whitespace;

proper line_offset;

clarified message severity, based on empirical observation of VSCode 1.8.1;

avoid escape of '/' in JSONFormat.quoteString;

more liberal drive letter, for the sake of file:// URLs;

clarified master_dir: file-URL;

A few new lemmas and needed adaptations

updated package;

avoid hardwired options: use isabelle.args settings instead;

support for Windows;

proper bootstrap name, e.g. for Pure.thy;

more robust startup;

more specific isabelle-ml language support;

tuned;

proper use of isabelle-ml;

grammar for Isabelle/ML, based on https://github.com/textmate/standard-ml.tmbundle/blob/fea2448/Syntaxes/Standard%20ML.plist

clarified multiple tooltips;

proper content format;

more syntax; tuned;

more syntax; tuned;

tuned;

tuned;

more keywords;

tuned;

proper packaging;

generate uuid;

generate static TextMate grammar for VSCode editor;

proper default;

clarified file name;

tuned;

more configuration;

automatically build session image;

tuned signature;

just one synchronized access to global state: works recursively on JVM; tuned;