src/Tools/VSCode/src/vscode_rendering.scala
2 months ago ago tuned signature;
6 months ago ago more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);
14 months ago ago more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
18 months ago ago tuned signature;
23 months ago ago retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
23 months ago ago clarified platform file operations;
23 months ago ago more completion;
23 months ago ago tuned signature;
23 months ago ago more completion;
23 months ago ago tuned signature;
23 months ago ago tuned signature;
23 months ago ago tuned signature;
23 months ago ago tuned signature;
23 months ago ago proper treatment of empty result;
23 months ago ago clarified modules;
23 months ago ago tuned signature;
23 months ago ago provide spell-checker menu via completion commands;
23 months ago ago added spell-checker completion;
23 months ago ago tuned signature;
23 months ago ago clarified signature;
23 months ago ago tuned;
23 months ago ago tuned;
23 months ago ago more uniform syntax_completion + semantic_completion;
2017-05-25 ago parallel retrieval of PIDE markup;
2017-05-23 ago support text overview colors via decorations;
2017-04-17 ago tuned signature;
2017-04-17 ago tuned signature;
2017-03-13 ago proper local debugger state, depending on session;
2017-03-12 ago discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
2017-03-10 ago suppress irrelevant markup for VSCode;
2017-03-10 ago avoid extra decorations for regular command keywords;
2017-03-10 ago more compact protocol message;
2017-03-07 ago decorations for text color;
2017-03-07 ago tuned;
2017-03-07 ago decorations for spell-checker;
2017-03-07 ago tuned signature;
2017-03-07 ago clarified options;
2017-03-06 ago clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
2017-03-05 ago decorations for dotted underline: less intrusive;
2017-03-05 ago proper reset of published decorations: initial value is Nil, afterwards it is a list of canonical length and order;
2017-03-04 ago clarified pretty margin;
2017-03-04 ago more general hover_message (see also JEdit_Rendering.tooltip_message);
2017-03-04 ago clarified signature;
2017-03-04 ago decorations for background and foreground colors;
2017-03-03 ago publish decorations like diagnostics;
2017-01-11 ago support for semantic completion;
2017-01-11 ago clarified text output wrt. symbols;
2017-01-08 ago added node_name(String): imitate jEdit buffer operations;
2017-01-08 ago support for bibtex entries;
2017-01-08 ago more explocit Document_Model.Content;
2017-01-07 ago clarified lazy text content;
2017-01-05 ago suppress empty results;
2017-01-04 ago tuned;
2017-01-04 ago proper interpretation of Resources.source_file as platform file;
2017-01-04 ago clarified Document.Node.Name (again): canonical platform file;
2017-01-04 ago clarified file URIs;
2017-01-03 ago clarified message severity, based on empirical observation of VSCode 1.8.1;
2017-01-03 ago clarified master_dir: file-URL;
2017-01-01 ago clarified modules;
2016-12-30 ago tuned;