Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. updated version;
  2. more robust (see https://code.visualstudio.com/docs/extensionAPI/document-selectors);
  3. tuned;
  4. more comment markup;
Changeset 69323:7698ad5d7036 by wenzelm:
updated version;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 69322:ce6d43af5bcb by wenzelm:
more robust (see https://code.visualstudio.com/docs/extensionAPI/document-selectors);
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 69321:42b91ee343ee by wenzelm:
tuned;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 69320:fc221fa79741 by wenzelm:
more comment markup;
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Tools/Haskell/Haskell.thy (diff)
The file was modified src/Tools/Haskell/Markup.hs (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/jEdit/etc/options (diff)