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;
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)