Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- merged
- avoid exhaustion of worker threads, notably due to complex interaction of future/promise/lazy in Proofterm.make_thm_node;
- more robust: insist in finished future;
- unused;
The file was modified | src/Pure/Concurrent/future.ML |
The file was modified | src/Pure/Concurrent/future.ML |
The file was modified | src/Pure/Concurrent/lazy.ML |
The file was modified | src/Pure/Concurrent/future.ML |