# HG changeset patch
# User wenzelm
# Date 1365018523 -7200
# Node ID 2843cc095a579e8eb40fa1d88d5be781562c5b4e
# Parent  eca8acb42e4a74808403312a85a483e3274631d3
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;

diff -r eca8acb42e4a -r 2843cc095a57 src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Wed Apr 03 21:30:32 2013 +0200
+++ b/src/Pure/General/timing.ML	Wed Apr 03 21:48:43 2013 +0200
@@ -23,6 +23,7 @@
   val is_relevant_time: Time.time -> bool
   val is_relevant: timing -> bool
   val message: timing -> string
+  val status: ('a -> 'b) -> 'a -> 'b
 end
 
 structure Timing: TIMING =
@@ -89,10 +90,10 @@
 fun cond_timeit enabled msg e =
   if enabled then
     let
-      val (timing, result) = timing (Exn.interruptible_capture e) ();
+      val (t, result) = timing (Exn.interruptible_capture e) ();
       val _ =
-        if is_relevant timing then
-          let val end_msg = message timing
+        if is_relevant t then
+          let val end_msg = message t
           in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end
         else ();
     in Exn.release result end
@@ -102,6 +103,12 @@
 fun timeap f x = timeit (fn () => f x);
 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
 
+fun status f x =
+  let
+    val (t, result) = timing (Exn.interruptible_capture f) x;
+    val _ = if is_relevant t then Output.status (Markup.markup_only (Markup.timing t)) else ();
+  in Exn.release result end;
+
 end;
 
 structure Basic_Timing: BASIC_TIMING = Timing;
diff -r eca8acb42e4a -r 2843cc095a57 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Apr 03 21:30:32 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 03 21:48:43 2013 +0200
@@ -1163,7 +1163,7 @@
     state |> future_proof (fn state' =>
       Goal.fork_params
         {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
-        (fn () => ((), proof2 state'))) |> snd |> done
+        (fn () => ((), Timing.status proof2 state'))) |> snd |> done
   else proof1 state;
 
 in
diff -r eca8acb42e4a -r 2843cc095a57 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Apr 03 21:30:32 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Apr 03 21:48:43 2013 +0200
@@ -94,14 +94,14 @@
   val cpuN: string
   val gcN: string
   val timing_propertiesN: string list
-  val timing_properties: Timing.timing -> Properties.T
-  val parse_timing_properties: Properties.T -> Timing.timing
+  val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
+  val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time}
   val command_timingN: string
   val command_timing_properties:
     {file: string, offset: int, name: string} -> Time.time -> Properties.T
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
-  val timingN: string val timing: Timing.timing -> T
+  val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
diff -r eca8acb42e4a -r 2843cc095a57 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Apr 03 21:30:32 2013 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 03 21:48:43 2013 +0200
@@ -28,9 +28,9 @@
 
 use "General/properties.ML";
 use "General/output.ML";
-use "General/timing.ML";
 use "PIDE/markup.ML";
 fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
+use "General/timing.ML";
 use "General/scan.ML";
 use "General/source.ML";
 use "General/symbol.ML";