moved multithreaded "profile" to multithreading_polyml.ML;
authorwenzelm
Tue Mar 25 12:14:17 2008 +0100 (2008-03-25)
changeset 2639099d4cbb1f941
parent 26389 3835c431e141
child 26391 6e8aa5a4eb82
moved multithreaded "profile" to multithreading_polyml.ML;
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/polyml-5.1.ML
src/Pure/ML-Systems/polyml.ML
     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
     2.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 25 11:52:15 2008 +0100
     2.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 25 12:14:17 2008 +0100
     2.3 @@ -10,12 +10,3 @@
     2.4  
     2.5  val pointer_eq = PolyML.pointerEq;
     2.6  
     2.7 -
     2.8 -(* single-threaded profiling *)
     2.9 -
    2.10 -local val profile_orig = profile in
    2.11 -
    2.12 -fun profile 0 f x = f x
    2.13 -  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
    2.14 -
    2.15 -end;
     3.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 11:52:15 2008 +0100
     3.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 12:14:17 2008 +0100
     3.3 @@ -10,17 +10,7 @@
     3.4  val pointer_eq = PolyML.pointerEq;
     3.5  
     3.6  
     3.7 -(* single-threaded profiling *)
     3.8 -
     3.9 -local val profile_orig = profile in
    3.10 -
    3.11 -fun profile 0 f x = f x
    3.12 -  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
    3.13 -
    3.14 -end;
    3.15 -
    3.16 -
    3.17 -(* improved versions of use_text/file *)
    3.18 +(* runtime compilation *)
    3.19  
    3.20  fun use_text (tune: string -> string) (line, name) (print, err) verbose txt =
    3.21    let