Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper edits;
  2. suppress vacuous messages;
  3. clarified modules;
  4. more explicit message type: allows body to become empty;
  5. clarified current_command: index refers to node content, negative index means first command;
Changeset 65203:314246c6eeaa by wenzelm:
proper edits;
The file was modified src/Pure/PIDE/line.scala (diff)
Changeset 65202:187277b77d50 by wenzelm:
suppress vacuous messages;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 65201:2d01b30e6ac6 by wenzelm:
clarified modules;
The file was addedsrc/Tools/VSCode/extension/src/protocol.ts
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/src/protocol.scala (diff)
Changeset 65200:1227a68fac7a by wenzelm:
more explicit message type: allows body to become empty;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
Changeset 65199:6bd7081f8319 by wenzelm:
clarified current_command: index refers to node content, negative index means first command;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Tools/VSCode/src/document_model.scala (diff)
The file was modified src/Tools/VSCode/src/dynamic_output.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)