Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned granularity of parallel tasks;
  3. more completion;
  4. clarified modules;
  5. tuned signature;
Changeset 66161:c6e9c7d140ff by wenzelm:
merged
Changeset 66160:33f759742887 by wenzelm:
tuned granularity of parallel tasks;
The file was modified etc/options (diff)
Changeset 66159:907720561c82 by wenzelm:
more completion;
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
Changeset 66158:ad83d4971dfe by wenzelm:
clarified modules;
The file was modified etc/options (diff)
The file was modified src/Doc/JEdit/JEdit.thy (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Tools/jEdit/etc/options (diff)
The file was modified src/Tools/jEdit/src/completion_popup.scala (diff)
Changeset 66157:cb57fcdbaf70 by wenzelm:
tuned signature;
The file was modified src/Pure/General/completion.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
The file was modified src/Tools/jEdit/src/completion_popup.scala (diff)