Summary
- merged;
- more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
- more synchronized Execution.snapshot;
- tuned spelling;
- tuned;
- tuned;
The file was modified | src/Pure/Concurrent/future.ML (diff) |
The file was modified | src/Pure/PIDE/execution.ML (diff) |
The file was modified | src/Pure/Thy/thy_info.ML (diff) |
The file was modified | src/Pure/PIDE/execution.ML (diff) |
The file was modified | src/Pure/PIDE/protocol.ML (diff) |
The file was modified | src/Pure/Thy/thy_info.ML (diff) |
The file was modified | src/Pure/PIDE/document.ML (diff) |
The file was modified | src/Pure/Thy/thy_info.ML (diff) |
The file was modified | src/Pure/PIDE/document.ML (diff) |