# HG changeset patch
# User wenzelm
# Date 1623228757 -7200
# Node ID 95484bd7e1ec8c310d2c7d31c2b01af954de3eea
# Parent  a5200fa7cb4c70ab6da0ffac58110ca171938f5b
proper profiling within command execution: messages require PIDE id;

diff -r a5200fa7cb4c -r 95484bd7e1ec src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Jun 09 10:37:53 2021 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Jun 09 10:52:37 2021 +0200
@@ -194,7 +194,8 @@
   f |> debugging1 opt_context |> debugging2 opt_context;
 
 fun controlled_execution opt_context f x =
-  (f |> debugging opt_context |> Future.interruptible_task) x;
+  (f |> debugging opt_context |> Future.interruptible_task
+    |> ML_Profiling.profile (Options.default_string "profiling")) x;
 
 fun toplevel_error output_exn f x = f x
   handle exn =>
diff -r a5200fa7cb4c -r 95484bd7e1ec src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Wed Jun 09 10:37:53 2021 +0200
+++ b/src/Pure/Tools/build.ML	Wed Jun 09 10:52:37 2021 +0200
@@ -46,7 +46,7 @@
 
 fun build_theories qualifier (options, thys) =
   let
-    val profiling = Options.string options "profiling" |> tap ML_Profiling.check_mode;
+    val _ = ML_Profiling.check_mode (Options.string options "profiling");
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
     val loaded_theories =
@@ -55,7 +55,6 @@
           Isabelle_Process.init_options ();
           Future.fork I;
           (Thy_Info.use_theories options qualifier
-          |> ML_Profiling.profile profiling
           |> Unsynchronized.setmp print_mode
               (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
       else