src/Tools/VSCode/src/server.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 support for workspace edits;
22 months ago wenzelm 2017-09-18 store document version;
23 months ago wenzelm 2017-08-10 tuned;
2017-07-01 wenzelm 2017-07-01 all_known can cause timeout of VSCode server startup, notably on Windows;
2017-06-29 wenzelm 2017-06-29 clarified editor focus;
2017-06-29 wenzelm 2017-06-29 proper hyperlink_command, notably for locate_query; support bidirectional caret update;
2017-06-29 wenzelm 2017-06-29 HTML GUI actions via JavaScript;
2017-06-20 wenzelm 2017-06-20 added commands for spell-checker dictionary;
2017-06-17 wenzelm 2017-06-17 maintain overlays within main state of document models; proper pending_input for Isabelle/VSCode;
2017-06-16 wenzelm 2017-06-16 proper treatment of editor overlays;
2017-06-16 wenzelm 2017-06-16 clarified modules;
2017-06-16 wenzelm 2017-06-16 support for separate proof state output;
2017-06-16 wenzelm 2017-06-16 more general dispatcher operations;
2017-06-13 wenzelm 2017-06-13 clarified signature;
2017-06-13 wenzelm 2017-06-13 added abstract editor operations, notably for Query_Operation;
2017-06-09 wenzelm 2017-06-09 more uniform syntax_completion + semantic_completion;
2017-06-09 wenzelm 2017-06-09 provide information about Isabelle symbols within VSCode;
2017-05-31 wenzelm 2017-05-31 explicit preview request/response; commands, icons, menus like VSCode markdown preview; clarified Uri information (again); tuned;
2017-05-30 wenzelm 2017-05-30 provide preview content on Scala side (similar to output);
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 clarified message logging;
2017-04-19 wenzelm 2017-04-19 always explore all sessions;
2017-04-03 wenzelm 2017-04-03 tuned signature;
2017-03-18 wenzelm 2017-03-18 more informative session result;
2017-03-15 wenzelm 2017-03-15 always output proof state: there is only one output buffer in Isabelle/VSCode;
2017-03-15 wenzelm 2017-03-15 dynamic session_options for tuning parameters and initial prover options;
2017-03-15 wenzelm 2017-03-15 clarified modules;
2017-03-14 wenzelm 2017-03-14 normalize changes strictly as specified in the protocol definition (assuming non-overlapping ranges, amending 0f555ce33970), e.g. relevant for automatic quotes/parentheses around selection;
2017-03-14 wenzelm 2017-03-14 avoid race condition between current_state().stable_tip_version and model.rendering();
2017-03-14 wenzelm 2017-03-14 tuned;
2017-03-14 wenzelm 2017-03-14 explicitly ignore "initialized" message;
2017-03-14 wenzelm 2017-03-14 clarified shutdown;
2017-03-14 wenzelm 2017-03-14 tuned;
2017-03-13 wenzelm 2017-03-13 tuned signature;
2017-03-13 wenzelm 2017-03-13 tuned signature;
2017-03-13 wenzelm 2017-03-13 clarified Session.Phase;
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-11 wenzelm 2017-03-11 support for caret handling and dynamic output;
2017-03-11 wenzelm 2017-03-11 apply multiple edits bottom-to-top as specified in the protocol definition (assuming canonical order);
2017-03-09 wenzelm 2017-03-09 tuned;
2017-03-09 wenzelm 2017-03-09 incremental document changes;
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-06 wenzelm 2017-03-06 more general tooltips, with uniform info range handling;
2017-03-05 wenzelm 2017-03-05 always invoke output: pending_output may be present due to other reasons;
2017-03-05 wenzelm 2017-03-05 simplified;
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 pretty margin;
2017-03-03 wenzelm 2017-03-03 clarified signature;
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-09 wenzelm 2017-01-09 tuned;
2017-01-09 wenzelm 2017-01-09 clarified modules; tuned;
2017-01-09 wenzelm 2017-01-09 tuned signature;
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 more informative error for spurious crash;
2017-01-05 wenzelm 2017-01-05 tuned;