src/Pure/ML-Systems/thread_dummy.ML
changeset 32736 f126e68d003d
parent 29564 f8b933a62151
child 32776 1504f9c2d060
equal deleted inserted replaced
32735:f96f3ae3a19d 32736:f126e68d003d
    32 struct
    32 struct
    33   type thread = unit;
    33   type thread = unit;
    34 
    34 
    35   datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
    35   datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
    36     and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
    36     and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
       
    37 
       
    38   fun unavailable () = fail ();
    37 
    39 
    38   fun fork _ = fail ();
    40   fun fork _ = fail ();
    39   fun exit _ = fail ();
    41   fun exit _ = fail ();
    40   fun isActive _ = fail ();
    42   fun isActive _ = fail ();
    41 
    43