Summary
- clarified Document.length -- independent of text_length;
- more robust shutdown;
- watcher for file-system events;
- tuned comments;
The file was modified | src/Pure/PIDE/line.scala (diff) |
The file was modified | src/Pure/General/file_watcher.scala (diff) |
The file was added | src/Pure/General/file_watcher.scala |
The file was modified | src/Pure/build-jars (diff) |
The file was modified | src/Pure/General/file.ML (diff) |
The file was modified | src/Pure/General/file.scala (diff) |