# HG changeset patch
# User wenzelm
# Date 1206443657 -3600
# Node ID 99d4cbb1f941fb37b15a978c88bcacacddf9e309
# Parent  3835c431e1410cd81eecd0ee810af2d026935c38
moved multithreaded "profile" to multithreading_polyml.ML;

diff -r 3835c431e141 -r 99d4cbb1f941 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 25 11:52:15 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 25 12:14:17 2008 +0100
@@ -13,6 +13,7 @@
   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 =
@@ -320,6 +321,16 @@
   in ! status 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
diff -r 3835c431e141 -r 99d4cbb1f941 src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 25 11:52:15 2008 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 25 12:14:17 2008 +0100
@@ -10,12 +10,3 @@
 
 val pointer_eq = PolyML.pointerEq;
 
-
-(* single-threaded 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;
diff -r 3835c431e141 -r 99d4cbb1f941 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 11:52:15 2008 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 12:14:17 2008 +0100
@@ -10,17 +10,7 @@
 val pointer_eq = PolyML.pointerEq;
 
 
-(* single-threaded 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;
-
-
-(* improved versions of use_text/file *)
+(* runtime compilation *)
 
 fun use_text (tune: string -> string) (line, name) (print, err) verbose txt =
   let