src/Tools/Haskell/Haskell.thy
changeset 69496 5256e7f26640
parent 69495 c34dfa431b89
child 69497 c434ca819aea
equal deleted inserted replaced
69495:c34dfa431b89 69496:5256e7f26640
  1689 
  1689 
  1690 module Isabelle.Standard_Thread (
  1690 module Isabelle.Standard_Thread (
  1691   ThreadId, Result,
  1691   ThreadId, Result,
  1692   find_id,
  1692   find_id,
  1693   properties, change_properties,
  1693   properties, change_properties,
  1694   stop, is_stopped,
  1694   is_stopped, stop,
       
  1695   my_uuid, stop_uuid,
  1695   Fork, fork_finally, fork)
  1696   Fork, fork_finally, fork)
  1696 where
  1697 where
  1697 
  1698 
  1698 import Data.Maybe
  1699 import Data.Maybe
  1699 import Data.IORef
  1700 import Data.IORef
  1700 import System.IO.Unsafe
  1701 import System.IO.Unsafe
  1701 
  1702 
  1702 import qualified Data.List as List
  1703 import qualified Data.List as List
       
  1704 import Control.Monad (forM_)
  1703 import Data.Map.Strict (Map)
  1705 import Data.Map.Strict (Map)
  1704 import qualified Data.Map.Strict as Map
  1706 import qualified Data.Map.Strict as Map
  1705 import Control.Exception.Base (SomeException)
  1707 import Control.Exception.Base (SomeException)
  1706 import Control.Exception as Exception
  1708 import Control.Exception as Exception
  1707 import Control.Concurrent (ThreadId)
  1709 import Control.Concurrent (ThreadId)
  1775 is_stopped :: IO Bool
  1777 is_stopped :: IO Bool
  1776 is_stopped = stopped <$> my_info
  1778 is_stopped = stopped <$> my_info
  1777 
  1779 
  1778 stop :: ThreadId -> IO ()
  1780 stop :: ThreadId -> IO ()
  1779 stop id = map_info id (\info -> info {stopped = True})
  1781 stop id = map_info id (\info -> info {stopped = True})
       
  1782 
       
  1783 
       
  1784 {- UUID -}
       
  1785 
       
  1786 my_uuid :: IO UUID.T
       
  1787 my_uuid = uuid <$> my_info
       
  1788 
       
  1789 stop_uuid :: UUID.T -> IO ()
       
  1790 stop_uuid uuid = do
       
  1791   id <- find_id uuid
       
  1792   forM_ id stop
  1780 
  1793 
  1781 
  1794 
  1782 {- fork -}
  1795 {- fork -}
  1783 
  1796 
  1784 type Fork a = (ThreadId, UUID.T, IO (Result a))
  1797 type Fork a = (ThreadId, UUID.T, IO (Result a))