src/Tools/VSCode/src/document_model.scala
22 months ago wenzelm 2017-09-18 recode Unicode text on the spot, e.g. from copy-paste of output;
22 months ago wenzelm 2017-09-18 store document version;
2017-06-21 wenzelm 2017-06-21 tuned signature;
2017-06-19 wenzelm 2017-06-19 clarified signature;
2017-06-16 wenzelm 2017-06-16 proper treatment of editor overlays;
2017-06-09 wenzelm 2017-06-09 more uniform syntax_completion + semantic_completion;
2017-05-25 wenzelm 2017-05-25 restricted perspective depending on the caret -- important for reactivity when editing big files;
2017-05-25 wenzelm 2017-05-25 tuned;
2017-04-03 wenzelm 2017-04-03 provide session qualifier via resources;
2017-03-13 wenzelm 2017-03-13 proper local debugger state, depending on session; tuned signature;
2017-03-12 wenzelm 2017-03-12 clarified current_command: index refers to node content, negative index means first command;
2017-03-12 wenzelm 2017-03-12 clarified caret offset; show output at end of file;
2017-03-12 wenzelm 2017-03-12 tuned signature;
2017-03-12 wenzelm 2017-03-12 discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
2017-03-11 wenzelm 2017-03-11 dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
2017-03-09 wenzelm 2017-03-09 clarified;
2017-03-09 wenzelm 2017-03-09 incremental document changes;
2017-03-07 wenzelm 2017-03-07 tuned signature;
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-05 wenzelm 2017-03-05 publish output more thoroughly;
2017-03-05 wenzelm 2017-03-05 more robust treatment of pending input/output: these are often correlated; no decorations for invisible node;
2017-03-04 wenzelm 2017-03-04 clarified signature;
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-10 wenzelm 2017-01-10 support "purge" operation on document model;
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 uniform Document.Model.node_edits (without void edits);
2017-01-07 wenzelm 2017-01-07 clarified check_thy_reader: check node_name here;
2017-01-07 wenzelm 2017-01-07 tuned signature;
2017-01-07 wenzelm 2017-01-07 tuned signature;
2017-01-07 wenzelm 2017-01-07 clarified lazy text content;
2017-01-07 wenzelm 2017-01-07 tuned;
2017-01-07 wenzelm 2017-01-07 tuned;
2017-01-06 wenzelm 2017-01-06 tuned;
2017-01-05 wenzelm 2017-01-05 more robust treatment of logical lines;
2017-01-05 wenzelm 2017-01-05 manage document blobs as well;
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-01 wenzelm 2017-01-01 clarified file URI operations;
2016-12-31 wenzelm 2016-12-31 automatically resolve dependencies from document models and file-system;
2016-12-31 wenzelm 2016-12-31 clarified;
2016-12-31 wenzelm 2016-12-31 tuned;
2016-12-31 wenzelm 2016-12-31 clarified node_visible;
2016-12-30 wenzelm 2016-12-30 manage changes of external files; tuned;
2016-12-30 wenzelm 2016-12-30 more explicit edits -- eliminated Clear;
2016-12-30 wenzelm 2016-12-30 clarified Document_Model perspective and edits;
2016-12-29 wenzelm 2016-12-29 re-use options from resources;
2016-12-29 wenzelm 2016-12-29 moved main state to VSCode_Resources; misc tuning;
2016-12-29 wenzelm 2016-12-29 re-use resources from session;
2016-12-28 wenzelm 2016-12-28 more uniform pending_input / pending_output; explicit Document_Model.uri; tuned;
2016-12-28 wenzelm 2016-12-28 clarified signature: maintan Text.Length within Line.Document;
2016-12-28 wenzelm 2016-12-28 clarified modules;
2016-12-28 wenzelm 2016-12-28 tuned;
2016-12-28 wenzelm 2016-12-28 more uniform treatment of input/output wrt. client; support for diagnistic messages; misc tuning;
2016-12-26 wenzelm 2016-12-26 more uniform treatment of file name vs. theory name and special header;
2016-12-26 wenzelm 2016-12-26 clarified document: no stored text;
2016-12-26 wenzelm 2016-12-26 clarified header text;
2016-12-23 wenzelm 2016-12-23 full range for Position.Item; more hyperlinks for VSCode;
2016-12-21 wenzelm 2016-12-21 tuned signature -- more explicit types;