# HG changeset patch
# User wenzelm
# Date 1695308696 -7200
# Node ID 1b9e0f74addbe2c5edea4ec27ce5399e15a7275c
# Parent  a98e0a816d28f42ade130fc47718678eda7868a7
more robust: prefer linear data flow;

diff -r a98e0a816d28 -r 1b9e0f74addb src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Wed Sep 20 17:40:09 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Thu Sep 21 17:04:56 2023 +0200
@@ -84,11 +84,15 @@
 
 fun fork (params: params) body =
   let
-    val name = #name params;
-    val id = make_id ();
-    fun main () = (set_self (make {thread = Thread.Thread.self (), name = name, id = id}); body ());
-    val thread = Thread.Thread.fork (main, attributes params);
-  in make {thread = thread, name = name, id = id} end;
+    val self = Single_Assignment.var "self";
+    fun main () =
+      let
+        val t = make {thread = Thread.Thread.self (), name = #name params, id = make_id ()};
+        val _ = set_self t;
+        val _ = Single_Assignment.assign self t;
+      in body () end;
+    val _ = Thread.Thread.fork (main, attributes params);
+  in Single_Assignment.await self end;
 
 
 (* join *)
diff -r a98e0a816d28 -r 1b9e0f74addb src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Sep 20 17:40:09 2023 +0200
+++ b/src/Pure/ROOT.ML	Thu Sep 21 17:04:56 2023 +0200
@@ -121,8 +121,8 @@
 ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
+ML_file "Concurrent/single_assignment.ML";
 ML_file "Concurrent/isabelle_thread.ML";
-ML_file "Concurrent/single_assignment.ML";
 
 ML_file "Concurrent/par_exn.ML";
 ML_file "Concurrent/task_queue.ML";