# HG changeset patch
# User wenzelm
# Date 1623076826 -7200
# Node ID 364bac6691dee476ca3515a3c686711865290168
# Parent  5153fad491f36484fa16b2b9ecc7f23ce7e29242
clarified modules;

diff -r 5153fad491f3 -r 364bac6691de src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Jun 07 15:13:34 2021 +0200
+++ b/src/Pure/General/output.ML	Mon Jun 07 16:40:26 2021 +0200
@@ -10,9 +10,6 @@
   val tracing: string -> unit
   val warning: string -> unit
   val legacy_feature: string -> unit
-  val profile_time: ('a -> 'b) -> 'a -> 'b
-  val profile_time_thread: ('a -> 'b) -> 'a -> 'b
-  val profile_allocations: ('a -> 'b) -> 'a -> 'b
 end;
 
 signature OUTPUT =
@@ -158,40 +155,6 @@
 fun protocol_message props body = ! protocol_message_fn props body;
 fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => ();
 
-
-(* profiling *)
-
-local
-
-fun output_profile title entries =
-  let
-    val body = entries
-      |> sort (int_ord o apply2 fst)
-      |> map (fn (count, name) =>
-          let
-            val c = string_of_int count;
-            val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
-          in prefix ^ c ^ " " ^ name end);
-    val total = fold (curry (op +) o fst) entries 0;
-  in
-    if total = 0 then ()
-    else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
-  end;
-
-in
-
-fun profile_time f x =
-  ML_Profiling.profile_time (output_profile "time profile:") f x;
-
-fun profile_time_thread f x =
-  ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x;
-
-fun profile_allocations f x =
-  ML_Profiling.profile_allocations (output_profile "allocations profile:") f x;
-
-end;
-
-
 end;
 
 structure Output: OUTPUT = Private_Output;
diff -r 5153fad491f3 -r 364bac6691de src/Pure/ML/ml_profiling.ML
--- a/src/Pure/ML/ml_profiling.ML	Mon Jun 07 15:13:34 2021 +0200
+++ b/src/Pure/ML/ml_profiling.ML	Mon Jun 07 16:40:26 2021 +0200
@@ -6,21 +6,39 @@
 
 signature ML_PROFILING =
 sig
-  val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
-  val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
-  val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
+  val profile_time: ('a -> 'b) -> 'a -> 'b
+  val profile_time_thread: ('a -> 'b) -> 'a -> 'b
+  val profile_allocations: ('a -> 'b) -> 'a -> 'b
 end;
 
 structure ML_Profiling: ML_PROFILING =
 struct
 
-fun profile_time pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+fun profile mode title =
+  mode |> PolyML.Profiling.profileStream (fn entries =>
+    let
+      val body = entries
+        |> sort (int_ord o apply2 fst)
+        |> map (fn (count, name) =>
+            let
+              val c = string_of_int count;
+              val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
+            in prefix ^ c ^ " " ^ name end);
+      val total = fold (curry (op +) o fst) entries 0;
+    in
+      if total = 0 then ()
+      else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
+    end);
 
-fun profile_time_thread pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+fun profile_time f =
+  profile PolyML.Profiling.ProfileTime "time profile:" f;
 
-fun profile_allocations pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+fun profile_time_thread f =
+  profile PolyML.Profiling.ProfileTimeThisThread "time profile (this thread):" f;
+
+fun profile_allocations f =
+  profile PolyML.Profiling.ProfileAllocations "allocations profile:" f;
 
 end;
+
+open ML_Profiling;
diff -r 5153fad491f3 -r 364bac6691de src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jun 07 15:13:34 2021 +0200
+++ b/src/Pure/ROOT.ML	Mon Jun 07 16:40:26 2021 +0200
@@ -27,7 +27,6 @@
 ML_file "Concurrent/counter.ML";
 
 ML_file "ML/ml_heap.ML";
-ML_file "ML/ml_profiling.ML";
 ML_file "ML/ml_print_depth0.ML";
 ML_file "ML/ml_pretty.ML";
 ML_file "ML/ml_compiler0.ML";
@@ -47,6 +46,7 @@
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
 ML_file "PIDE/markup.ML";
+ML_file "ML/ml_profiling.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
 ML_file "General/source.ML";