Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. manage changes of external files; tuned;
  3. more explicit edits -- eliminated Clear;
  4. tuned;
  5. clarified Document_Model perspective and edits;
  6. tuned;
Changeset 64711:45dfaad6d852 by wenzelm:
merged
Changeset 64710:72ca4e5f976e by wenzelm:
manage changes of external files;<br>tuned;
The file was modified src/Pure/General/file_watcher.scala (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 64709:5e6566ab78bf by wenzelm:
more explicit edits -- eliminated Clear;
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 64708:dd7f1a7e03f4 by wenzelm:
tuned;
The file was modified src/Tools/VSCode/src/server.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
Changeset 64707:7157685b71e3 by wenzelm:
clarified Document_Model perspective and edits;
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 64706:3ebf9f8299df by wenzelm:
tuned;
The file was modified src/Tools/VSCode/src/server.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)