Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned -- like Dynamic_Preview;
  3. tuned;
  4. provide preview content on Scala side (similar to output);
  5. tuned signature;
  6. more careful treatment of context.subscriptions;
  7. clarified event handling; tuned;
  8. tuned;
  9. clarified modules;
  10. tuned;
  11. clarified modules;
  12. tuned imports;
  13. clarified modules;
  14. clarified signature;
  15. clarified modules;
Changeset 65980:3bec939bd808 by wenzelm:
merged
Changeset 65979:c208fcf369b7 by wenzelm:
tuned -- like Dynamic_Preview;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/extension/src/protocol.ts (diff)
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
Changeset 65978:5754708a2d05 by wenzelm:
tuned;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 65977:c51b74be23b6 by wenzelm:
provide preview content on Scala side (similar to output);
The file was addedsrc/Tools/VSCode/src/dynamic_preview.scala
The file was modified src/Pure/build-jars (diff)
The file was modified src/Tools/VSCode/etc/options (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/extension/src/preview.ts (diff)
The file was modified src/Tools/VSCode/extension/src/protocol.ts (diff)
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
The file was modified src/Tools/VSCode/src/server.scala (diff)
Changeset 65976:1448d71fbd22 by wenzelm:
tuned signature;
The file was modified src/Tools/VSCode/src/dynamic_output.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
Changeset 65975:f20739a63a44 by wenzelm:
more careful treatment of context.subscriptions;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 65974:fd5f80ee2de0 by wenzelm:
clarified event handling;<br>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)
The file was modified src/Tools/VSCode/extension/src/preview.ts (diff)
Changeset 65973:84ea75759b77 by wenzelm:
tuned;
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
Changeset 65972:9f6a154c6ca0 by wenzelm:
clarified modules;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/extension/src/library.ts (diff)
Changeset 65971:81aadb4e7fdf by wenzelm:
tuned;
The file was modified src/Tools/VSCode/extension/src/preview.ts (diff)
Changeset 65970:05e317e291a8 by wenzelm:
clarified modules;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/extension/src/library.ts (diff)
Changeset 65969:1f93eb5c3d77 by wenzelm:
tuned imports;
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 65968:44e703278dfd by wenzelm:
clarified modules;
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/extension/src/library.ts (diff)
Changeset 65967:5d9da2f8fd3f by wenzelm:
clarified signature;
The file was modified src/Tools/VSCode/extension/src/library.ts (diff)
The file was modified src/Tools/VSCode/extension/src/preview.ts (diff)
Changeset 65966:169d2928cce1 by wenzelm:
clarified modules;
The file was addedsrc/Tools/VSCode/extension/src/library.ts
The file was modified src/Tools/VSCode/extension/src/preview.ts (diff)