Skip to content
Success

Changes

Summary

  1. updated package;
  2. prefer immutable bindings;
  3. tuned;
  4. tuned;
  5. updated to vscode-languageclient 3.0;
  6. more thorough build;
  7. clarified versions;
  8. tuned;
  9. clarified;
  10. incremental document changes;
  11. proper treatment of line that becomes empty;
  12. tuned;
  13. clarified Document.offset: including final position; support Document.change according to VSCode;
  14. suppress vacuous edits;
  15. clarified native Text.Offset versus Text.Length index Int;
  16. tuned;
  17. tuned;
  18. tuned messages;
Changeset 65169:a8dfa258bf93 by wenzelm:
updated package;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 65168:9eabc312a2a2 by wenzelm:
prefer immutable bindings;
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 65167:ee569aac344b by wenzelm:
tuned;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 65166:f8aafbf2b02e by wenzelm:
tuned;
The file was modified src/HOL/Hahn_Banach/Hahn_Banach.thy (diff)
Changeset 65165:d98ede9e5917 by wenzelm:
updated to vscode-languageclient 3.0;
The file was modified src/Tools/VSCode/extension/package.json (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
Changeset 65164:6cbb894181c8 by wenzelm:
more thorough build;
The file was modified src/Tools/VSCode/src/build_vscode.scala (diff)
Changeset 65163:d596a070f039 by wenzelm:
clarified versions;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 65162:df1052d0708d by wenzelm:
tuned;
The file was modified src/Tools/VSCode/src/server.scala (diff)
Changeset 65161:6af056380d0b by wenzelm:
clarified;
The file was modified src/Tools/VSCode/src/document_model.scala (diff)
Changeset 65160:6e042537555d by wenzelm:
incremental document changes;
The file was modified src/Tools/VSCode/src/document_model.scala (diff)
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
The file was modified src/Tools/VSCode/src/server.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
Changeset 65159:0ae97858d8b3 by wenzelm:
proper treatment of line that becomes empty;
The file was modified src/Pure/PIDE/line.scala (diff)
Changeset 65158:b87a972b965d by wenzelm:
tuned;
The file was modified src/Tools/VSCode/README.md (diff)
Changeset 65157:cd977a5bd928 by wenzelm:
clarified Document.offset: including final position;<br>support Document.change according to VSCode;
The file was modified src/Pure/PIDE/line.scala (diff)
Changeset 65156:35fefc249311 by wenzelm:
suppress vacuous edits;
The file was modified src/Pure/PIDE/text.scala (diff)
Changeset 65155:25bccf5bf33e by wenzelm:
clarified native Text.Offset versus Text.Length index Int;
The file was modified src/Pure/PIDE/text.scala (diff)
Changeset 65154:ba1929b749f0 by wenzelm:
tuned;
The file was modified src/Pure/PIDE/text.scala (diff)
Changeset 65153:82bd5d29adbf by wenzelm:
tuned;
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 65152:a920012ae16a by wenzelm:
tuned messages;
The file was modified src/Tools/VSCode/src/channel.scala (diff)