Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. support VSCode DocumentHighlights; clarified modules;
  3. clarified file URLs, notably for Windows UNC paths;
  4. more language support;
  5. tuned whitespace;
  6. proper line_offset;
  7. clarified message severity, based on empirical observation of VSCode 1.8.1;
  8. avoid escape of '/' in JSONFormat.quoteString;
  9. more liberal drive letter, for the sake of file:// URLs;
  10. clarified master_dir: file-URL;
Changeset 64768:34ef44748370 by wenzelm:
merged
Changeset 64767:f5c4ffdb1124 by wenzelm:
support VSCode DocumentHighlights;<br>clarified modules;
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
The file was modified src/Tools/VSCode/src/server.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 64766:6fd05caf55f0 by wenzelm:
clarified file URLs, notably for Windows UNC paths;
The file was modified src/Pure/General/url.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
Changeset 64765:8ae1af3f88b1 by wenzelm:
more language support;
The file was modified src/Tools/VSCode/extension/isabelle-language.json (diff)
Changeset 64764:452b4fb7927c by wenzelm:
tuned whitespace;
The file was modified src/Tools/VSCode/extension/isabelle-language.json (diff)
The file was modified src/Tools/VSCode/extension/isabelle-ml-language.json (diff)
Changeset 64763:20e498a28f5e by wenzelm:
proper line_offset;
The file was modified src/Pure/PIDE/line.scala (diff)
Changeset 64762:cd545bec3fd0 by wenzelm:
clarified message severity, based on empirical observation of VSCode 1.8.1;
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
Changeset 64761:ae97a5afffcc by wenzelm:
avoid escape of &#039;/&#039; in JSONFormat.quoteString;
The file was modified src/Pure/General/json.scala (diff)
Changeset 64760:8c1557308eb5 by wenzelm:
more liberal drive letter, for the sake of file:// URLs;
The file was modified src/Pure/General/file.scala (diff)
Changeset 64759:100941134718 by wenzelm:
clarified master_dir: file-URL;
The file was modified src/Pure/General/file.scala (diff)
The file was modified src/Pure/General/url.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Thy/thy_header.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)