Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. superseded by external protocol;
  2. use old-style "textEdit" for the sake of the external protocol (see also vscode-languageserver-node/issues/188);
  3. tuned;
  4. symbol completion that bypasses the LS protocol, and thus observes the range properly; more symbol operations;
  5. More rules for Probability/Tree_Space
Changeset 66063:a2e441805d6a by wenzelm:
superseded by external protocol;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 66062:175772371cd0 by wenzelm:
use old-style "textEdit" for the sake of the external protocol (see also vscode-languageserver-node/issues/188);
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
Changeset 66061:880db47fed30 by wenzelm:
tuned;
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
Changeset 66060:b2bfbefd354f by wenzelm:
symbol completion that bypasses the LS protocol, and thus observes the range properly;<br>more symbol operations;
The file was addedsrc/Tools/VSCode/extension/src/completion.ts
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/extension/src/symbol.ts (diff)
Changeset 66059:5a6b67e42c4a by eberlm _eberlm@in.tum.de_:
More rules for Probability/Tree_Space
The file was modified src/HOL/Probability/Tree_Space.thy (diff)