Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned colors;
  2. apply multiple edits bottom-to-top as specified in the protocol definition (assuming canonical order);
  3. tuned colors;
  4. proper Map operations; re-init decorations after configuration change;
  5. tuned colors according to Light+ and Dark+ themes;
  6. tuned signature;
Changeset 65185:663bb1614d23 by wenzelm:
tuned colors;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 65184:0f555ce33970 by wenzelm:
apply multiple edits bottom-to-top as specified in the protocol definition (assuming canonical order);
The file was modified src/Tools/VSCode/src/server.scala (diff)
Changeset 65183:37f1effd6683 by wenzelm:
tuned colors;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 65182:973b7669e7d9 by wenzelm:
proper Map operations;<br>re-init decorations after configuration change;
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 65181:b4105202751c by wenzelm:
tuned colors according to Light+ and Dark+ themes;
The file was modified src/Tools/VSCode/extension/package.json (diff)
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
Changeset 65180:b5a8f27a4980 by wenzelm:
tuned signature;
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)