Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;
authorwenzelm
Fri, 09 Jan 2015 20:12:42 +0100
changeset 59330 cb3a4caf206d
parent 59329 72278d083d3a
child 59331 4139db32821e
permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;
src/Pure/Concurrent/future.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Concurrent/future.ML	Fri Jan 09 19:20:00 2015 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Jan 09 20:12:42 2015 +0100
@@ -264,7 +264,9 @@
 
 fun worker_start name = (*requires SYNCHRONIZED*)
   Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
-    Unsynchronized.ref Working));
+    Unsynchronized.ref Working))
+  handle Fail msg => Multithreading.tracing 0 (fn () => msg);
+
 
 
 (* scheduler *)
isabelle