src/Pure/ML-Systems/multithreading_polyml.ML
changeset 26390 99d4cbb1f941
parent 26254 3def1a1fea4e
child 26493 de4764e95166
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 25 11:52:15 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 25 12:14:17 2008 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4    val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
     1.5    val system_out: string -> string * int
     1.6    structure TimeLimit: TIME_LIMIT
     1.7 +  val profile: int -> ('a -> 'b) -> 'a -> 'b
     1.8  end;
     1.9  
    1.10  signature BASIC_MULTITHREADING =
    1.11 @@ -320,6 +321,16 @@
    1.12    in ! status end);
    1.13  
    1.14  
    1.15 +(* profiling *)
    1.16 +
    1.17 +local val profile_orig = profile in
    1.18 +
    1.19 +fun profile 0 f x = f x
    1.20 +  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
    1.21 +
    1.22 +end;
    1.23 +
    1.24 +
    1.25  (* serial numbers *)
    1.26  
    1.27  local