more systematic treatment of profiling mode;

--- a/src/Pure/ML/ml_profiling.ML	Tue Jun 08 23:36:30 2021 +0200
+++ b/src/Pure/ML/ml_profiling.ML	Wed Jun 09 10:37:53 2021 +0200
@@ -1,50 +1,76 @@
 (*  Title:      Pure/ML/ml_profiling.ML
     Author:     Makarius
 
-ML profiling.
+ML profiling (via Poly/ML run-time system).
 *)
 
-signature ML_PROFILING =
+signature BASIC_ML_PROFILING =
 sig
   val profile_time: ('a -> 'b) -> 'a -> 'b
   val profile_time_thread: ('a -> 'b) -> 'a -> 'b
   val profile_allocations: ('a -> 'b) -> 'a -> 'b
 end;
 
+signature ML_PROFILING =
+sig
+  val check_mode: string -> unit
+  val profile: string -> ('a -> 'b) -> 'a -> 'b
+  include BASIC_ML_PROFILING
+end;
+
 structure ML_Profiling: ML_PROFILING =
 struct
 
+(* mode *)
+
+val modes =
+  Symtab.make
+    [("time", PolyML.Profiling.ProfileTime),
+     ("time_thread", PolyML.Profiling.ProfileTimeThisThread),
+     ("allocations", PolyML.Profiling.ProfileAllocations)];
+
+fun get_mode kind =
+  (case Symtab.lookup modes kind of
+    SOME mode => mode
+  | NONE => error ("Bad profiling mode: " ^ quote kind));
+
+fun check_mode "" = ()
+  | check_mode kind = ignore (get_mode kind);
+
+
+(* profile *)
+
 fun print_entry count name =
   let
     val c = string_of_int count;
     val prefix = Symbol.spaces (Int.max (0, 10 - size c));
   in prefix ^ c ^ " " ^ name end;
 
-fun profile mode kind title f x =
-  PolyML.Profiling.profileStream (fn entries =>
-    (case fold (curry (op +) o fst) entries 0 of
-      0 => ()
-    | total =>
-        let
-          val body = entries
-            |> sort (int_ord o apply2 fst)
-            |> map (fn (count, name) =>
-                let val markup = Markup.ML_profiling_entry {name = name, count = count}
-                in XML.Elem (markup, [XML.Text (print_entry count name ^ "\n")]) end);
-          val xml =
-            XML.Elem (Markup.ML_profiling kind,
-              XML.Text (title ^ "\n") :: body @ [XML.Text (print_entry total "TOTAL")]);
-        in tracing (YXML.string_of xml) end)) mode f x;
+fun profile "" f x = f x
+  | profile kind f x =
+      let
+        val mode = get_mode kind;
+        fun output entries =
+          (case fold (curry (op +) o fst) entries 0 of
+            0 => ()
+          | total =>
+              let
+                val body = entries
+                  |> sort (int_ord o apply2 fst)
+                  |> map (fn (count, name) =>
+                      let val markup = Markup.ML_profiling_entry {name = name, count = count}
+                      in XML.Elem (markup, [XML.Text (print_entry count name ^ "\n")]) end);
+                val head = XML.Text ("profile_" ^ kind ^ ":\n");
+                val foot = XML.Text (print_entry total "TOTAL");
+                val msg = XML.Elem (Markup.ML_profiling kind, head :: body @ [foot]);
+              in tracing (YXML.string_of msg) end);
+      in PolyML.Profiling.profileStream output mode f x end;
 
-fun profile_time f =
-  profile PolyML.Profiling.ProfileTime "time" "time profile:" f;
-
-fun profile_time_thread f =
-  profile PolyML.Profiling.ProfileTimeThisThread "time_thread" "time profile (single thread):" f;
-
-fun profile_allocations f =
-  profile PolyML.Profiling.ProfileAllocations "allocations" "allocations profile:" f;
+fun profile_time f = profile "time" f;
+fun profile_time_thread f = profile "time_thread" f;
+fun profile_allocations f = profile "allocations" f;
 
 end;
 
-open ML_Profiling;
+structure Basic_ML_Profiling: BASIC_ML_PROFILING = ML_Profiling;
+open Basic_ML_Profiling;

--- a/src/Pure/ML/ml_profiling.scala	Tue Jun 08 23:36:30 2021 +0200
+++ b/src/Pure/ML/ml_profiling.scala	Wed Jun 09 10:37:53 2021 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/ML/ml_profiling.scala
     Author:     Makarius
 
-ML profiling.
+ML profiling (via Poly/ML run-time system).
 */
 
 package isabelle
@@ -30,10 +30,7 @@
     def total: Entry = Entry("TOTAL", entries.iterator.map(_.count).sum)
 
     def print: String =
-    {
-      (if (kind == "time_thread") "time profile (single thread)" else kind + " profile") +
-        (entries ::: List(total)).map(_.print).mkString(":\n", "\n", "")
-    }
+      ("profile_" + kind + ":\n") + cat_lines((entries ::: List(total)).map(_.print))
   }
 
   def account(reports: List[Report]): List[Report] =

--- a/src/Pure/Tools/build.ML	Tue Jun 08 23:36:30 2021 +0200
+++ b/src/Pure/Tools/build.ML	Wed Jun 09 10:37:53 2021 +0200
@@ -46,6 +46,7 @@
 
 fun build_theories qualifier (options, thys) =
   let
+    val profiling = Options.string options "profiling" |> tap ML_Profiling.check_mode;
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
     val loaded_theories =
@@ -54,12 +55,7 @@
           Isabelle_Process.init_options ();
           Future.fork I;
           (Thy_Info.use_theories options qualifier
-          |>
-            (case Options.string options "profiling" of
-              "" => I
-            | "time" => profile_time
-            | "allocations" => profile_allocations
-            | bad => error ("Bad profiling option: " ^ quote bad))
+          |> ML_Profiling.profile profiling
           |> Unsynchronized.setmp print_mode
               (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
       else