| changeset 73841 | 95484bd7e1ec |
| parent 70603 | 706dac15554b |
| child 78679 | dc7455787a8e |
--- 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 =>