added enabled;
authorwenzelm
Thu Oct 09 20:53:24 2008 +0200 (2008-10-09)
changeset 28555d59712ee942c
parent 28554 a6065ce44984
child 28556 85d2972fe9e6
added enabled;
removed pseudo-parallel version of profile -- CRITICAL prevents future join;
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 09 20:53:23 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 09 20:53:24 2008 +0200
     1.3 @@ -11,7 +11,6 @@
     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 @@ -46,6 +45,8 @@
    1.12    let val m = ! max_threads
    1.13    in if m <= 0 then Int.max (Thread.numProcessors (), 1) else m end;
    1.14  
    1.15 +fun enabled () = max_threads_value () > 1;
    1.16 +
    1.17  
    1.18  (* misc utils *)
    1.19  
    1.20 @@ -226,16 +227,6 @@
    1.21  end;
    1.22  
    1.23  
    1.24 -(* profiling *)
    1.25 -
    1.26 -local val profile_orig = profile in
    1.27 -
    1.28 -fun profile 0 f x = f x
    1.29 -  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
    1.30 -
    1.31 -end;
    1.32 -
    1.33 -
    1.34  (* serial numbers *)
    1.35  
    1.36  local