src/Tools/VSCode/src/vscode_rendering.scala
2017-03-10 wenzelm 2017-03-10 suppress irrelevant markup for VSCode;
2017-03-10 wenzelm 2017-03-10 avoid extra decorations for regular command keywords;
2017-03-10 wenzelm 2017-03-10 more compact protocol message;
2017-03-07 wenzelm 2017-03-07 decorations for text color;
2017-03-07 wenzelm 2017-03-07 tuned;
2017-03-07 wenzelm 2017-03-07 decorations for spell-checker;
2017-03-07 wenzelm 2017-03-07 tuned signature;
2017-03-07 wenzelm 2017-03-07 clarified options;
2017-03-06 wenzelm 2017-03-06 clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover); discontinued obsolete "hover_message" decoration;
2017-03-05 wenzelm 2017-03-05 decorations for dotted underline: less intrusive; tuned;
2017-03-05 wenzelm 2017-03-05 proper reset of published decorations: initial value is Nil, afterwards it is a list of canonical length and order;
2017-03-04 wenzelm 2017-03-04 clarified pretty margin;
2017-03-04 wenzelm 2017-03-04 more general hover_message (see also JEdit_Rendering.tooltip_message);
2017-03-04 wenzelm 2017-03-04 clarified signature;
2017-03-04 wenzelm 2017-03-04 decorations for background and foreground colors;
2017-03-03 wenzelm 2017-03-03 publish decorations like diagnostics; Markup.BAD is decoration, not error message;
2017-01-11 wenzelm 2017-01-11 support for semantic completion;
2017-01-11 wenzelm 2017-01-11 clarified text output wrt. symbols;
2017-01-08 wenzelm 2017-01-08 added node_name(String): imitate jEdit buffer operations; more uniform get_file_content for external source file references;
2017-01-08 wenzelm 2017-01-08 support for bibtex entries;
2017-01-08 wenzelm 2017-01-08 more explocit Document_Model.Content;
2017-01-07 wenzelm 2017-01-07 clarified lazy text content;
2017-01-05 wenzelm 2017-01-05 suppress empty results;
2017-01-04 wenzelm 2017-01-04 tuned;
2017-01-04 wenzelm 2017-01-04 proper interpretation of Resources.source_file as platform file;
2017-01-04 wenzelm 2017-01-04 clarified Document.Node.Name (again): canonical platform file; identify document models by native java.io.File;
2017-01-04 wenzelm 2017-01-04 clarified file URIs;
2017-01-03 wenzelm 2017-01-03 clarified message severity, based on empirical observation of VSCode 1.8.1;
2017-01-03 wenzelm 2017-01-03 clarified master_dir: file-URL;
2017-01-01 wenzelm 2017-01-01 clarified modules;
2016-12-30 wenzelm 2016-12-30 tuned;
2016-12-29 wenzelm 2016-12-29 re-use options from resources;
2016-12-29 wenzelm 2016-12-29 re-use resources from session;
2016-12-28 wenzelm 2016-12-28 precise full_range and thus proper try_restrict in Snapshot.cumulate;
2016-12-28 wenzelm 2016-12-28 clarified signature: maintan Text.Length within Line.Document;
2016-12-28 wenzelm 2016-12-28 more uniform treatment of input/output wrt. client; support for diagnistic messages; misc tuning;
2016-12-23 wenzelm 2016-12-23 proper file:// URL for external references;
2016-12-23 wenzelm 2016-12-23 full range for Position.Item; more hyperlinks for VSCode;
2016-12-23 wenzelm 2016-12-23 removed junk;
2016-12-21 wenzelm 2016-12-21 clarified signature;
2016-12-21 wenzelm 2016-12-21 VSCode already detects URLs from plain text;
2016-12-21 wenzelm 2016-12-21 clarified signature;
2016-12-21 wenzelm 2016-12-21 tuned signature -- more explicit types;
2016-12-21 wenzelm 2016-12-21 basic support for hyperlinks / Goto Definition Request;
2016-12-20 wenzelm 2016-12-20 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;