equal
deleted
inserted
replaced
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)) |