diff --git a/src/Pure/Isar/runtime.ML b/src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML
+++ b/src/Pure/Isar/runtime.ML
@@ -1,214 +1,215 @@
 (*  Title:      Pure/Isar/runtime.ML
     Author:     Makarius
 
 Isar toplevel runtime support.
 *)
 
 signature RUNTIME =
 sig
   exception UNDEF
   exception EXCURSION_FAIL of exn * string
   exception TOPLEVEL_ERROR
   val pretty_exn: exn -> Pretty.T
   val exn_context: Proof.context option -> exn -> exn
   val thread_context: exn -> exn
   type error = ((serial * string) * string option)
   val exn_messages: exn -> error list
   val exn_message_list: exn -> string list
   val exn_message: exn -> string
   val exn_error_message: exn -> unit
   val exn_system_message: exn -> unit
   val exn_trace: (unit -> 'a) -> 'a
   val exn_trace_system: (unit -> 'a) -> 'a
   val exn_debugger: (unit -> 'a) -> 'a
   val exn_debugger_system: (unit -> 'a) -> 'a
   val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
   val toplevel_program: (unit -> 'a) -> 'a
 end;
 
 structure Runtime: RUNTIME =
 struct
 
 (** exceptions **)
 
 exception UNDEF;
 exception EXCURSION_FAIL of exn * string;
 exception TOPLEVEL_ERROR;
 
 
 (* pretty *)
 
 fun pretty_exn (exn: exn) =
   Pretty.from_ML
     (ML_Pretty.from_polyml
       (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))));
 
 
 (* exn_context *)
 
 exception CONTEXT of Proof.context * exn;
 
 fun exn_context NONE exn = exn
   | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
 
 fun thread_context exn =
   exn_context (Option.map Context.proof_of (Context.get_generic_context ())) exn;
 
 
 (* exn_message *)
 
 type error = ((serial * string) * string option);
 
 local
 
 fun robust f x =
   (case try f x of
     SOME s => s
   | NONE => Markup.markup Markup.intensify "<malformed>");
 
 fun robust2 f x y = robust (fn () => f x y) ();
 
 fun robust_context NONE _ _ = []
   | robust_context (SOME ctxt) f xs = map (robust2 f ctxt) xs;
 
 fun identify exn =
   let
     val exn' = Par_Exn.identify [] exn;
     val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
     val i = Par_Exn.the_serial exn' handle Option.Option => serial ();
   in ((i, exn'), exec_id) end;
 
 fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
   | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
   | flatten context exn =
       (case Par_Exn.dest exn of
         SOME exns => maps (flatten context) exns
       | NONE => [(context, identify exn)]);
 
 val print_thy = Pretty.unformatted_string_of o Context.pretty_abbrev_thy;
 
 in
 
 fun exn_messages e =
   let
     fun raised exn name msgs =
       let val pos = Position.here (Exn_Properties.position exn) in
         (case msgs of
           [] => "exception " ^ name ^ " raised" ^ pos
         | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
         | _ =>
             cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") ::
               map (Markup.markup Markup.item) msgs))
       end;
 
     fun exn_msgs (context, ((i, exn), id)) =
       (case exn of
         EXCURSION_FAIL (exn, loc) =>
           map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
             (sorted_msgs context exn)
       | _ =>
         let
           val msg =
             (case exn of
               Timeout.TIMEOUT t => Timeout.print t
             | TOPLEVEL_ERROR => "Error"
             | ERROR "" => "Error"
             | ERROR msg => msg
             | Fail msg => raised exn "Fail" [msg]
             | THEORY (msg, thys) => raised exn "THEORY" (msg :: map (robust print_thy) thys)
             | Ast.AST (msg, asts) =>
                 raised exn "AST" (msg :: map (robust (Pretty.string_of o Ast.pretty_ast)) asts)
             | TYPE (msg, Ts, ts) =>
                 raised exn "TYPE" (msg ::
                   (robust_context context Syntax.string_of_typ Ts @
                     robust_context context Syntax.string_of_term ts))
             | TERM (msg, ts) =>
                 raised exn "TERM" (msg :: robust_context context Syntax.string_of_term ts)
             | CTERM (msg, cts) =>
                 raised exn "CTERM"
                   (msg :: robust_context context Syntax.string_of_term (map Thm.term_of cts))
             | THM (msg, i, thms) =>
                 raised exn ("THM " ^ string_of_int i)
                   (msg :: robust_context context Thm.string_of_thm thms)
             | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
         in [((i, msg), id)] end)
       and sorted_msgs context exn =
         sort_distinct (int_ord o apply2 (fst o fst)) (maps exn_msgs (flatten context exn));
 
   in sorted_msgs NONE e end;
 
 end;
 
 fun exn_message_list exn =
   (case exn_messages exn of
     [] => ["Interrupt"]
   | msgs => map (#2 o #1) msgs);
 
 val exn_message = cat_lines o exn_message_list;
 
 val exn_error_message = Output.error_message o exn_message;
 val exn_system_message = Output.system_message o exn_message;
 fun exn_trace e = Exn.trace exn_message tracing e;
 fun exn_trace_system e = Exn.trace exn_message Output.system_message e;
 
 
 (* exception debugger *)
 
 local
 
 fun print_entry (name, loc) =
   Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_polyml_location loc));
 
 fun exception_debugger output e =
   let
     val (trace, result) = Exn_Debugger.capture_exception_trace e;
     val _ =
       (case (trace, result) of
         (_ :: _, Exn.Exn exn) =>
           output (cat_lines ("Exception trace - " ^ exn_message exn :: map print_entry trace))
       | _ => ());
   in Exn.release result end;
 
 in
 
 fun exn_debugger e = exception_debugger tracing e;
 fun exn_debugger_system e = exception_debugger Output.system_message e;
 
 end;
 
 
 
 (** controlled execution **)
 
 fun debugging1 opt_context f x =
   if ML_Options.exception_trace_enabled opt_context
   then exn_trace (fn () => f x) else f x;
 
 fun debugging2 opt_context f x =
   if ML_Options.exception_debugger_enabled opt_context
   then exn_debugger (fn () => f x) else f x;
 
 fun debugging opt_context f =
   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 =>
     if Exn.is_interrupt exn then Exn.reraise exn
     else
       let
         val opt_ctxt =
           (case Context.get_generic_context () of
             NONE => NONE
           | SOME context => try Context.proof_of context);
         val _ = output_exn (exn_context opt_ctxt exn);
       in raise TOPLEVEL_ERROR end;
 
 fun toplevel_program body =
   (body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
 
 end;
diff --git a/src/Pure/Tools/build.ML b/src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML
+++ b/src/Pure/Tools/build.ML
@@ -1,116 +1,115 @@
 (*  Title:      Pure/Tools/build.ML
     Author:     Makarius
 
 Build Isabelle sessions.
 *)
 
 signature BUILD =
 sig
   type hook = string -> (theory * Document_Output.segment list) list -> unit
   val add_hook: hook -> unit
 end;
 
 structure Build: BUILD =
 struct
 
 (* session timing *)
 
 fun session_timing f x =
   let
     val start = Timing.start ();
     val y = f x;
     val timing = Timing.result start;
 
     val threads = string_of_int (Multithreading.max_threads ());
     val props = [("threads", threads)] @ Markup.timing_properties timing;
     val _ = Output.protocol_message (Markup.session_timing :: props) [];
   in y end;
 
 
 (* build theories *)
 
 type hook = string -> (theory * Document_Output.segment list) list -> unit;
 
 local
   val hooks = Synchronized.var "Build.hooks" ([]: hook list);
 in
 
 fun add_hook hook = Synchronized.change hooks (cons hook);
 
 fun apply_hooks qualifier loaded_theories =
   Synchronized.value hooks
   |> List.app (fn hook => hook qualifier loaded_theories);
 
 end;
 
 
 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 =
       if null conds then
         (Options.set_default options;
           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
        (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
           " (undefined " ^ commas conds ^ ")\n"); [])
   in apply_hooks qualifier loaded_theories end;
 
 
 (* build session *)
 
 val _ =
   Protocol_Command.define "build_session"
     (fn [resources_yxml, args_yxml] =>
         let
           val _ = Resources.init_session_yxml resources_yxml;
           val (session_name, theories) =
             YXML.parse_body args_yxml |>
               let
                 open XML.Decode;
                 val position = Position.of_properties o properties;
               in pair string (list (pair Options.decode (list (pair string position)))) end;
 
           val _ = Session.init session_name;
 
           fun build () =
             let
               val res1 =
                 theories |>
                   (List.app (build_theories session_name)
                     |> session_timing
                     |> Exn.capture);
               val res2 = Exn.capture Session.finish ();
 
               val _ = Resources.finish_session_base ();
               val _ = Par_Exn.release_all [res1, res2];
               val _ =
                 if session_name = Context.PureN
                 then Theory.install_pure (Thy_Info.get_theory Context.PureN) else ();
             in () end;
 
           fun exec e =
             if can Theory.get_pure () then
               Isabelle_Thread.fork
                 {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (),
                   interrupts = false} e
               |> ignore
             else e ();
         in
           exec (fn () =>
             (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn =>
               ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
           |> let open XML.Encode in pair int (list string) end
           |> single
           |> Output.protocol_message Markup.build_session_finished)
         end
       | _ => raise Match);
 
 end;