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;

clarified modules;

clarified file URI operations;

more precise markup; tuned signature;

automatically resolve dependencies from document models and file-system;

clarified;

tuned;

ignore message;

clarified node_visible;

tuned signature;

proper state update;

proper log;

tuned;

tuned signature;

tuned signature;

proper import_name;

more elementary rules about div / mod on int

complete set of cases rules for integers known to be (non-)positive/negative; legacy theorem branding

more facts on sgn, abs

dropped slightly outdated comment

merged

manage changes of external files; tuned;

more explicit edits -- eliminated Clear;

tuned;

clarified Document_Model perspective and edits;

tuned;

more uniform errors in '(prim)(co)rec(ursive)' variants

re-use options from resources;

moved main state to VSCode_Resources; misc tuning;

re-use resources from session;

clarified Document.length -- independent of text_length;

more robust shutdown;

watcher for file-system events;

tuned comments;

tuned;

publish extension on Visual Studio Marketplace;

updated VSCode extension to "isabelle vscode_server";

merged

DiagnosticSeverity according to implementation https://github.com/Microsoft/vscode-languageserver-node instead of documentation https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md;

support for syslog messages; clarified shutdown;

prefer stable state -- reduce repeated diagnostics;

more uniform pending_input / pending_output; explicit Document_Model.uri; tuned;

unused;

precise full_range and thus proper try_restrict in Snapshot.cumulate;

clarified protocol errors;

clarified signature;

unused;

clarified options;

clarified signature: maintan Text.Length within Line.Document;

clarified modules;

clarified signature: explicit Length to avoid implicit mistakes;

tuned;

more uniform treatment of input/output wrt. client; support for diagnistic messages; misc tuning;

tuned;

more uniform treatment of "bad" like other messages (with serial number);

clarified modules;

support for diagnostics;

print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'

more uniform treatment of file name vs. theory name and special header;

clarified document: no stored text;

clarified header text;

restored instance for char, which got ancidentally lost in b3f2b8c906a6

merged