# 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";