src/Pure/ML-Systems/multithreading_polyml.ML
changeset 26390 99d4cbb1f941
parent 26254 3def1a1fea4e
child 26493 de4764e95166
equal deleted inserted replaced
26389:3835c431e141 26390:99d4cbb1f941
    11 sig
    11 sig
    12   val interruptible: ('a -> 'b) -> 'a -> 'b
    12   val interruptible: ('a -> 'b) -> 'a -> 'b
    13   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
    13   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
    14   val system_out: string -> string * int
    14   val system_out: string -> string * int
    15   structure TimeLimit: TIME_LIMIT
    15   structure TimeLimit: TIME_LIMIT
       
    16   val profile: int -> ('a -> 'b) -> 'a -> 'b
    16 end;
    17 end;
    17 
    18 
    18 signature BASIC_MULTITHREADING =
    19 signature BASIC_MULTITHREADING =
    19 sig
    20 sig
    20   include BASIC_MULTITHREADING
    21   include BASIC_MULTITHREADING
   318        wait_timeout ())));
   319        wait_timeout ())));
   319 
   320 
   320   in ! status end);
   321   in ! status end);
   321 
   322 
   322 
   323 
       
   324 (* profiling *)
       
   325 
       
   326 local val profile_orig = profile in
       
   327 
       
   328 fun profile 0 f x = f x
       
   329   | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
       
   330 
       
   331 end;
       
   332 
       
   333 
   323 (* serial numbers *)
   334 (* serial numbers *)
   324 
   335 
   325 local
   336 local
   326 
   337 
   327 val serial_lock = Mutex.mutex ();
   338 val serial_lock = Mutex.mutex ();