# HG changeset patch
# User wenzelm
# Date 1223578404 -7200
# Node ID d59712ee942cf7dee0581e4f2e57170fe1e6a929
# Parent  a6065ce44984df4fbdbdfe7049b6ba9a79e65165
added enabled;
removed pseudo-parallel version of profile -- CRITICAL prevents future join;

diff -r a6065ce44984 -r d59712ee942c src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 09 20:53:23 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 09 20:53:24 2008 +0200
@@ -11,7 +11,6 @@
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
   val system_out: string -> string * int
   structure TimeLimit: TIME_LIMIT
-  val profile: int -> ('a -> 'b) -> 'a -> 'b
 end;
 
 signature BASIC_MULTITHREADING =
@@ -46,6 +45,8 @@
   let val m = ! max_threads
   in if m <= 0 then Int.max (Thread.numProcessors (), 1) else m end;
 
+fun enabled () = max_threads_value () > 1;
+
 
 (* misc utils *)
 
@@ -226,16 +227,6 @@
 end;
 
 
-(* profiling *)
-
-local val profile_orig = profile in
-
-fun profile 0 f x = f x
-  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
-
-end;
-
-
 (* serial numbers *)
 
 local