Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned signature;
  3. support "purge" operation on document model;
  4. proper template;
  5. tuned;
  6. accomodate very big file_models and changed_files;
  7. tuned;
Changeset 64869:a73ac9558220 by wenzelm:
merged
Changeset 64868:6212d3c396b0 by wenzelm:
tuned signature;
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
Changeset 64867:e7220f4de11f by wenzelm:
support "purge" operation on document model;
The file was modified NEWS (diff)
The file was modified src/Pure/General/file_watcher.scala (diff)
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/editor.scala (diff)
The file was modified src/Tools/VSCode/src/document_model.scala (diff)
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)
Changeset 64866:372c833c7660 by wenzelm:
proper template;
The file was modified src/Pure/PIDE/editor.scala (diff)
Changeset 64865:778c64c17363 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/info_dockable.scala (diff)
Changeset 64864:eec7ffef0be6 by wenzelm:
accomodate very big file_models and changed_files;
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
Changeset 64863:e5572c1169fd by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/document_model.scala (diff)