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 is_stopped, stop, |
1694 is_stopped, expose_stopped, stop, |
1695 my_uuid, stop_uuid, |
1695 my_uuid, stop_uuid, |
1696 Fork, fork_finally, fork) |
1696 Fork, fork_finally, fork) |
1697 where |
1697 where |
1698 |
1698 |
1699 import Data.Maybe |
1699 import Data.Maybe |
1700 import Data.IORef |
1700 import Data.IORef |
1701 import System.IO.Unsafe |
1701 import System.IO.Unsafe |
1702 |
1702 |
1703 import qualified Data.List as List |
1703 import qualified Data.List as List |
1704 import Control.Monad (forM_) |
1704 import Control.Monad (when, forM_) |
1705 import Data.Map.Strict (Map) |
1705 import Data.Map.Strict (Map) |
1706 import qualified Data.Map.Strict as Map |
1706 import qualified Data.Map.Strict as Map |
1707 import Control.Exception.Base (SomeException) |
1707 import Control.Exception.Base (SomeException) |
1708 import Control.Exception as Exception |
1708 import Control.Exception as Exception |
1709 import Control.Concurrent (ThreadId) |
1709 import Control.Concurrent (ThreadId) |
1774 |
1774 |
1775 {- stop -} |
1775 {- stop -} |
1776 |
1776 |
1777 is_stopped :: IO Bool |
1777 is_stopped :: IO Bool |
1778 is_stopped = stopped <$> my_info |
1778 is_stopped = stopped <$> my_info |
|
1779 |
|
1780 expose_stopped :: IO () |
|
1781 expose_stopped = do |
|
1782 stopped <- is_stopped |
|
1783 when stopped $ throw ThreadKilled |
1779 |
1784 |
1780 stop :: ThreadId -> IO () |
1785 stop :: ThreadId -> IO () |
1781 stop id = map_info id (\info -> info {stopped = True}) |
1786 stop id = map_info id (\info -> info {stopped = True}) |
1782 |
1787 |
1783 |
1788 |