Summary
- merged
- tuned signature;
- support "purge" operation on document model;
- proper template;
- tuned;
- accomodate very big file_models and changed_files;
- tuned;
The file was modified | src/Tools/jEdit/src/document_model.scala (diff) |
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) |
The file was modified | src/Pure/PIDE/editor.scala (diff) |
The file was modified | src/Tools/jEdit/src/info_dockable.scala (diff) |
The file was modified | src/Tools/jEdit/src/document_model.scala (diff) |
The file was modified | src/Tools/jEdit/src/document_model.scala (diff) |