more centralized command timing;
authorwenzelm
Tue Apr 02 11:41:50 2013 +0200 (2013-04-02 ago)
changeset 515958e9746e584c9
parent 51594 89bfe7a33615
child 51596 4f25e800f520
more centralized command timing;
clarified old-style timing message;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Apr 02 10:58:51 2013 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Apr 02 11:41:50 2013 +0200
     1.3 @@ -638,32 +638,39 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun timing_message tr (t: Timing.timing) =
     1.8 -  (case approximative_id tr of
     1.9 -    SOME id =>
    1.10 -      (Output.protocol_message
    1.11 -        (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
    1.12 -      handle Fail _ => ())
    1.13 -  | NONE => ());
    1.14 -
    1.15  fun app int (tr as Transition {trans, print, no_timing, ...}) =
    1.16    setmp_thread_position tr (fn state =>
    1.17      let
    1.18 -      fun do_timing f x = (warning (command_msg "" tr); timeap f x);
    1.19 -      fun do_profiling f x = profile (! profiling) f x;
    1.20 +      val timing_start = Timing.start ();
    1.21  
    1.22 -      val start = Timing.start ();
    1.23 -
    1.24 -      val (result, status) =
    1.25 +      val (result, opt_err) =
    1.26           state |>
    1.27            (apply_trans int trans
    1.28 -            |> (! profiling > 0 andalso not no_timing) ? do_profiling
    1.29 -            |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
    1.30 -
    1.31 +            |> (! profiling > 0 andalso not no_timing) ? profile (! profiling));
    1.32        val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
    1.33  
    1.34 -      val _ = timing_message tr (Timing.result start);
    1.35 -    in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
    1.36 +      val timing_result = Timing.result timing_start;
    1.37 +
    1.38 +      val _ =
    1.39 +        if Timing.is_relevant timing_result andalso
    1.40 +          (! profiling > 0 orelse ! timing andalso not no_timing)
    1.41 +        then warning (command_msg "" tr ^ ": " ^ Timing.message timing_result)
    1.42 +        else ();
    1.43 +      val _ =
    1.44 +        if Timing.is_relevant timing_result
    1.45 +        then status tr (Markup.timing timing_result)
    1.46 +        else ();
    1.47 +      val _ =
    1.48 +        (case approximative_id tr of
    1.49 +          SOME id =>
    1.50 +            (Output.protocol_message
    1.51 +              (Markup.command_timing ::
    1.52 +                Markup.command_timing_properties id (#elapsed timing_result)) ""
    1.53 +            handle Fail _ => ())
    1.54 +        | NONE => ());
    1.55 +    in
    1.56 +      (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err)
    1.57 +    end);
    1.58  
    1.59  in
    1.60  
     2.1 --- a/src/Pure/PIDE/command.ML	Tue Apr 02 10:58:51 2013 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Tue Apr 02 11:41:50 2013 +0200
     2.3 @@ -61,19 +61,10 @@
     2.4  
     2.5  local
     2.6  
     2.7 -fun timing tr t =
     2.8 -  if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
     2.9 -
    2.10  fun run int tr st =
    2.11    if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
    2.12 -    Toplevel.setmp_thread_position tr (fn () =>
    2.13 -      (Goal.fork_name "Toplevel.diag" ~1
    2.14 -        (fn () =>
    2.15 -          let
    2.16 -            val start = Timing.start ();
    2.17 -            val res = Exn.interruptible_capture (fn () => Toplevel.command_exception int tr st) ();
    2.18 -            val _ = timing tr (Timing.result start);
    2.19 -          in Exn.release res end); ([], SOME st))) ()
    2.20 +    (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st);
    2.21 +      ([], SOME st))
    2.22    else Toplevel.command_errors int tr st;
    2.23  
    2.24  fun check_cmts tr cmts st =
    2.25 @@ -106,11 +97,9 @@
    2.26  
    2.27        val _ = Multithreading.interrupted ();
    2.28        val _ = Toplevel.status tr Markup.running;
    2.29 -      val start = Timing.start ();
    2.30        val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    2.31        val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
    2.32        val errs = errs1 @ errs2;
    2.33 -      val _ = timing tr (Timing.result start);
    2.34        val _ = Toplevel.status tr Markup.finished;
    2.35        val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
    2.36      in