Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. update XML cache for slightly modified messages;
  3. more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
Changeset 67826:5ea76b219668 by wenzelm:
tuned;
The file was modified src/Pure/PIDE/command.scala (diff)
Changeset 67825:f9c071cc958b by wenzelm:
update XML cache for slightly modified messages;
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/session.scala (diff)
Changeset 67824:661cd25304ae by wenzelm:
more compact markup tree: output messages are already stored in command results (e.g. relevant for  XML data representation);
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)