Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. updated package;
  2. dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
  3. tuned;
  4. support for caret handling and dynamic output;
  5. more complete exception handling;
  6. tuned;
  7. tuned;
  8. tuned colors;
  9. apply multiple edits bottom-to-top as specified in the protocol definition (assuming canonical order);
  10. tuned colors;
  11. proper Map operations; re-init decorations after configuration change;
  12. tuned colors according to Light+ and Dark+ themes;
  13. tuned signature;
Changeset 65192:7b8dc3910b96 by wenzelm:
updated package;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 65191:4c9c83311cad by wenzelm:
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
The file was addedsrc/Tools/VSCode/src/dynamic_output.scala
The file was modified src/Pure/build-jars (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/src/document_model.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 65190:0dd2ad9dbfc2 by wenzelm:
tuned;
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
The file was modified src/Tools/jEdit/src/output_dockable.scala (diff)
Changeset 65189:41d2452845fc by wenzelm:
support for caret handling and dynamic output;
The file was modified src/Tools/VSCode/extension/src/extension.ts (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 65188:50cfc6775361 by wenzelm:
more complete exception handling;
The file was modified src/Pure/General/url.scala (diff)
Changeset 65187:9250f944ec0f by wenzelm:
tuned;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
Changeset 65186:4659e87c3795 by wenzelm:
tuned;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 65185:663bb1614d23 by wenzelm:
tuned colors;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 65184:0f555ce33970 by wenzelm:
apply multiple edits bottom-to-top as specified in the protocol definition (assuming canonical order);
The file was modified src/Tools/VSCode/src/server.scala (diff)
Changeset 65183:37f1effd6683 by wenzelm:
tuned colors;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 65182:973b7669e7d9 by wenzelm:
proper Map operations;<br>re-init decorations after configuration change;
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 65181:b4105202751c by wenzelm:
tuned colors according to Light+ and Dark+ themes;
The file was modified src/Tools/VSCode/extension/package.json (diff)
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
Changeset 65180:b5a8f27a4980 by wenzelm:
tuned signature;
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)