Summary
- more robust;
- less wasteful consolidation, based on PIDE front-end state and recent changes;
- tuned -- short-circuit result;
- tuned;
The file was modified | src/Pure/PIDE/session.scala (diff) |
The file was modified | etc/options (diff) |
The file was modified | src/Pure/PIDE/command.scala (diff) |
The file was modified | src/Pure/PIDE/document.ML (diff) |
The file was modified | src/Pure/PIDE/document.scala (diff) |
The file was modified | src/Pure/PIDE/protocol.ML (diff) |
The file was modified | src/Pure/PIDE/protocol.scala (diff) |
The file was modified | src/Pure/PIDE/resources.scala (diff) |
The file was modified | src/Pure/PIDE/session.scala (diff) |
The file was modified | src/Pure/Thy/thy_syntax.scala (diff) |
The file was modified | src/Pure/PIDE/document.ML (diff) |
The file was modified | src/Pure/Concurrent/future.ML (diff) |
The file was modified | src/Pure/PIDE/execution.ML (diff) |