# HG changeset patch
# User wenzelm
# Date 1545404520 -3600
# Node ID 7e44f8e2cc491b62319523bfd9fd1eab8886558a
# Parent  6fa742b0310753db08e35b83fb2072b2b9dbfd3d
more Haskell operations;

diff -r 6fa742b03107 -r 7e44f8e2cc49 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Fri Dec 21 13:38:44 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Fri Dec 21 16:02:00 2018 +0100
@@ -1689,15 +1689,17 @@
 
 module Isabelle.Standard_Thread (
   ThreadId, Result,
+  find_id,
   properties, change_properties,
   stop, is_stopped,
-  fork_finally, fork)
+  Fork, fork_finally, fork)
 where
 
 import Data.Maybe
 import Data.IORef
 import System.IO.Unsafe
 
+import qualified Data.List as List
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Control.Exception.Base (SomeException)
@@ -1706,19 +1708,20 @@
 import qualified Control.Concurrent as Concurrent
 import Control.Concurrent.Thread (Result)
 import qualified Control.Concurrent.Thread as Thread
+import qualified Isabelle.UUID as UUID
 import qualified Isabelle.Properties as Properties
 
 
 {- thread info -}
 
-data Info = Info {props :: Properties.T, stopped :: Bool}
+data Info = Info {uuid :: UUID.T, props :: Properties.T, stopped :: Bool}
 type Infos = Map ThreadId Info
 
 lookup_info :: Infos -> ThreadId -> Maybe Info
-lookup_info state id = Map.lookup id state
-
-init_info :: ThreadId -> Infos -> (Infos, ())
-init_info id infos = (Map.insert id (Info [] False) infos, ())
+lookup_info infos id = Map.lookup id infos
+
+init_info :: ThreadId -> UUID.T -> Infos -> (Infos, ())
+init_info id uuid infos = (Map.insert id (Info uuid [] False) infos, ())
 
 
 {- global state -}
@@ -1727,6 +1730,11 @@
 global_state :: IORef Infos
 global_state = unsafePerformIO (newIORef Map.empty)
 
+find_id :: UUID.T -> IO (Maybe ThreadId)
+find_id uuid = do
+  state <- readIORef global_state
+  return $ fst <$> List.find (\(_, Info{uuid = uuid'}) -> uuid == uuid') (Map.assocs state)
+
 get_info :: ThreadId -> IO (Maybe Info)
 get_info id = do
   state <- readIORef global_state
@@ -1769,19 +1777,22 @@
 
 {- fork -}
 
-fork_finally :: IO a -> (Either SomeException a -> IO b) -> IO (ThreadId, IO (Result b))
+type Fork a = (ThreadId, UUID.T, IO (Result a))
+
+fork_finally :: IO a -> (Either SomeException a -> IO b) -> IO (Fork b)
 fork_finally body finally = do
+  uuid <- UUID.random
   (id, result) <-
     Exception.mask (\restore ->
       Thread.forkIO
         (Exception.try
           (do
             id <- Concurrent.myThreadId
-            atomicModifyIORef' global_state (init_info id)
+            atomicModifyIORef' global_state (init_info id uuid)
             restore body) >>= finally))
-  return (id, result)
-
-fork :: IO a -> IO (ThreadId, IO (Result a))
+  return (id, uuid, result)
+
+fork :: IO a -> IO (Fork a)
 fork body = fork_finally body Thread.result
 \<close>