tuned;

tuned signature;

more operations for typed JSON values;

adapted to 3869b2400e22;

support for workspace edits;

retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;

clarified editor focus;

proper hyperlink_command, notably for locate_query;
support bidirectional caret update;

HTML GUI actions via JavaScript;

tuned signature;

provide spell-checker menu via completion commands;

added commands for spell-checker dictionary;

support for separate proof state output;

tuned;

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

tuned;

provide information about Isabelle symbols within VSCode;

explicit preview request/response;
commands, icons, menus like VSCode markdown preview;
clarified Uri information (again);
tuned;

--HG--
rename : src/Tools/VSCode/src/dynamic_preview.scala => src/Tools/VSCode/src/preview.scala

tuned -- like Dynamic_Preview;

provide preview content on Scala side (similar to output);

clarified output: do not require "method", which is absent for ResponseMessage;

clarified message logging;

explicitly ignore "initialized" message;

clarified modules;

more explicit message type: allows body to become empty;

support for caret handling and dynamic output;

more compact protocol message;

updated to vscode-languageclient 3.0;

incremental document changes;

more general hover_message (see also JEdit_Rendering.tooltip_message);

tight protocol messages;

publish decorations like diagnostics;
Markup.BAD is decoration, not error message;

support for decorations;

clarified signature;

tuned;

support for semantic completion;

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

support VSCode DocumentHighlights;
clarified modules;

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

proper content format;

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;

unused;

support for diagnostics;

clarified signature;

tuned signature -- more explicit types;

basic support for hyperlinks / Goto Definition Request;

basic support for VSCode Language Server protocol;
minimal extension for VSCode editor;