# HG changeset patch # User wenzelm # Date 1365531412 -7200 # Node ID 3391a493f39a7a10bedece602b553a639ea8143d # Parent 92e58b76dbb1e63a956cf5c6eae7bbfaaa17c238 just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build; diff -r 92e58b76dbb1 -r 3391a493f39a src/Pure/General/timing.ML --- a/src/Pure/General/timing.ML Tue Apr 09 15:59:02 2013 +0200 +++ b/src/Pure/General/timing.ML Tue Apr 09 20:16:52 2013 +0200 @@ -23,7 +23,8 @@ val is_relevant_time: Time.time -> bool val is_relevant: timing -> bool val message: timing -> string - val status: ('a -> 'b) -> 'a -> 'b + val protocol_message: Properties.T -> timing -> unit + val protocol: Properties.T -> ('a -> 'b) -> 'a -> 'b end structure Timing: TIMING = @@ -103,10 +104,13 @@ 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 = +fun protocol_message props t = + Output.try_protocol_message (props @ Markup.timing_properties t) ""; + +fun protocol props 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 (); + val _ = protocol_message props t; in Exn.release result end; end; diff -r 92e58b76dbb1 -r 3391a493f39a src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Apr 09 15:59:02 2013 +0200 +++ b/src/Pure/Isar/proof.ML Tue Apr 09 20:16:52 2013 +0200 @@ -1154,16 +1154,20 @@ end; -(* terminal proofs *) +(* terminal proofs *) (* FIXME avoid toplevel imitation -- include in PIDE/document *) local fun future_terminal_proof proof1 proof2 done int state = if Goal.future_enabled_level 3 andalso not (is_relevant state) then state |> future_proof (fn state' => - Goal.fork_params - {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1} - (fn () => ((), Timing.status proof2 state'))) |> snd |> done + let + val pos = Position.thread_data (); + val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos; + in + Goal.fork_params {name = "Proof.future_terminal_proof", pos = pos, pri = ~1} + (fn () => ((), Timing.protocol props proof2 state')) + end) |> snd |> done else proof1 state; in diff -r 92e58b76dbb1 -r 3391a493f39a src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Apr 09 15:59:02 2013 +0200 +++ b/src/Pure/Isar/toplevel.ML Tue Apr 09 20:16:52 2013 +0200 @@ -89,7 +89,6 @@ val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b val status: transition -> Markup.T -> unit val add_hook: (transition -> state -> state -> unit) -> unit - val approximative_id: transition -> {file: string, offset: int, name: string} option val get_timing: transition -> Time.time option val put_timing: Time.time option -> transition -> transition val transition: bool -> transition -> state -> (state * (exn * string) option) option @@ -591,19 +590,6 @@ fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr; -(* approximative identification within source file *) - -fun approximative_id tr = - let - val name = name_of tr; - val pos = pos_of tr; - in - (case (Position.file_of pos, Position.offset_of pos) of - (SOME file, SOME offset) => SOME {file = file, offset = offset, name = name} - | _ => NONE) - end; - - (* thread position *) fun setmp_thread_position (Transition {pos, ...}) f x = @@ -643,23 +629,9 @@ val _ = if int andalso not (! quiet) andalso print then print_state false result else (); val timing_result = Timing.result timing_start; - - val _ = - if Timing.is_relevant timing_result andalso (! profiling > 0 orelse ! timing) - andalso not (Keyword.is_control (name_of tr)) - then tracing (command_msg "" tr ^ ": " ^ Timing.message timing_result) - else (); - val _ = - if Timing.is_relevant timing_result - then status tr (Markup.timing timing_result) - else (); - val _ = - (case approximative_id tr of - SOME id => - (Output.try_protocol_message - (Markup.command_timing :: - Markup.command_timing_properties id (#elapsed timing_result)) "") - | NONE => ()); + val timing_props = + Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr); + val _ = Timing.protocol_message timing_props timing_result; in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err) end); diff -r 92e58b76dbb1 -r 3391a493f39a src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Apr 09 15:59:02 2013 +0200 +++ b/src/Pure/PIDE/markup.scala Tue Apr 09 20:16:52 2013 +0200 @@ -193,6 +193,7 @@ { def apply(timing: isabelle.Timing): Properties.T = Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds) + def unapply(props: Properties.T): Option[isabelle.Timing] = (props, props, props) match { case (Elapsed(elapsed), CPU(cpu), GC(gc)) => @@ -206,6 +207,7 @@ object Timing { def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing)) + def unapply(markup: Markup): Option[isabelle.Timing] = markup match { case Markup(TIMING, Timing_Properties(timing)) => Some(timing) @@ -214,6 +216,22 @@ } + /* command timing */ + + object Command_Timing + { + def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] = + props match { + case (FUNCTION, "command_timing") :: args => + (args, args) match { + case (Position.Id(id), Timing_Properties(timing)) => Some((id, timing)) + case _ => None + } + case _ => None + } + } + + /* toplevel */ val SUBGOALS = "subgoals" diff -r 92e58b76dbb1 -r 3391a493f39a src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Tue Apr 09 15:59:02 2013 +0200 +++ b/src/Pure/System/isar.ML Tue Apr 09 20:16:52 2013 +0200 @@ -118,6 +118,23 @@ local +fun protocol_message props output = + (case props of + function :: args => + if function = Markup.command_timing then + let + val name = the_default "" (Properties.get args Markup.nameN); + val pos = Position.of_properties args; + val timing = Markup.parse_timing_properties args; + in + if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing) + andalso name <> "" andalso not (Keyword.is_control name) + then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing) + else () + end + else raise Output.Protocol_Message props + | [] => raise Output.Protocol_Message props); + fun raw_loop secure src = let fun check_secure () = @@ -139,6 +156,7 @@ fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} = (Context.set_thread_data NONE; if do_init then (Options.load_default (); init ()) else (); + Output.Private_Hooks.protocol_message_fn := protocol_message; if welcome then writeln (Session.welcome ()) else (); uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ()); diff -r 92e58b76dbb1 -r 3391a493f39a src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Apr 09 15:59:02 2013 +0200 +++ b/src/Pure/System/session.scala Tue Apr 09 20:16:52 2013 +0200 @@ -300,22 +300,31 @@ def handle_output(output: Isabelle_Process.Output) //{{{ { - def bad_output(output: Isabelle_Process.Output) + def bad_output() { if (verbose) System.err.println("Ignoring prover output: " + output.message.toString) } + def accumulate(state_id: Document.ID, message: XML.Elem) + { + try { + val st = global_state >>> (_.accumulate(state_id, message)) + delay_commands_changed.invoke(false, List(st.command)) + } + catch { + case _: Document.State.Fail => bad_output() + } + } + output.properties match { case Position.Id(state_id) if !output.is_protocol => - try { - val st = global_state >>> (_.accumulate(state_id, output.message)) - delay_commands_changed.invoke(false, List(st.command)) - } - catch { - case _: Document.State.Fail => bad_output(output) - } + accumulate(state_id, output.message) + + case Markup.Command_Timing(state_id, timing) if output.is_protocol => + // FIXME XML.cache (!?) + accumulate(state_id, XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))) case Markup.Assign_Execs if output.is_protocol => XML.content(output.body) match { @@ -324,8 +333,8 @@ val cmds = global_state >>> (_.assign(id, assign)) delay_commands_changed.invoke(true, cmds) } - catch { case _: Document.State.Fail => bad_output(output) } - case _ => bad_output(output) + catch { case _: Document.State.Fail => bad_output() } + case _ => bad_output() } // FIXME separate timeout event/message!? if (prover.isDefined && System.currentTimeMillis() > prune_next) { @@ -340,8 +349,8 @@ try { global_state >> (_.removed_versions(removed)) } - catch { case _: Document.State.Fail => bad_output(output) } - case _ => bad_output(output) + catch { case _: Document.State.Fail => bad_output() } + case _ => bad_output() } case Markup.Invoke_Scala(name, id) if output.is_protocol => @@ -374,7 +383,7 @@ if (rc == 0) phase = Session.Inactive else phase = Session.Failed - case _ => bad_output(output) + case _ => bad_output() } } //}}} diff -r 92e58b76dbb1 -r 3391a493f39a src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Tue Apr 09 15:59:02 2013 +0200 +++ b/src/Pure/Tools/build.ML Tue Apr 09 20:16:52 2013 +0200 @@ -12,16 +12,56 @@ structure Build: BUILD = struct +(* command timings *) + +type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name * time *) + +val empty_timings: timings = Symtab.empty; + +fun update_timings props = + (case Markup.parse_command_timing_properties props of + SOME ({file, offset, name}, time) => + Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time))) + | NONE => I); + +fun approximative_id name pos = + (case (Position.file_of pos, Position.offset_of pos) of + (SOME file, SOME offset) => + if name = "" then NONE else SOME {file = file, offset = offset, name = name} + | _ => NONE); + +fun lookup_timings timings tr = + (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of + SOME {file, offset, name} => + (case Symtab.lookup timings file of + SOME offsets => + (case Inttab.lookup offsets offset of + SOME (name', time) => if name = name' then SOME time else NONE + | NONE => NONE) + | NONE => NONE) + | NONE => NONE); + + (* protocol messages *) -(* FIXME avoid hardwired stuff!? *) -val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing]; +fun inline_message a args = + writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args)); fun protocol_message props output = (case props of function :: args => - if member (op =) protocol_echo function then - writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args)) + if function = Markup.ML_statistics orelse function = Markup.task_statistics then + inline_message (#2 function) args + else if function = Markup.command_timing then + let + val name = the_default "" (Properties.get args Markup.nameN); + val pos = Position.of_properties args; + val {elapsed, ...} = Markup.parse_timing_properties args; + in + (case approximative_id name pos of + SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed) + | NONE => ()) + end else (case Markup.dest_loading_theory props of SOME name => writeln ("\floading_theory = " ^ name) @@ -74,30 +114,6 @@ " (undefined " ^ commas conds ^ ")\n")) end; - -(* command timings *) - -type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name * time *) - -val empty_timings: timings = Symtab.empty; - -fun update_timings props = - (case Markup.parse_command_timing_properties props of - SOME ({file, offset, name}, time) => - Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time))) - | NONE => I); - -fun lookup_timings timings tr = - (case Toplevel.approximative_id tr of - SOME {file, offset, name} => - (case Symtab.lookup timings file of - SOME offsets => - (case Inttab.lookup offsets offset of - SOME (name', time) => if name = name' then SOME time else NONE - | NONE => NONE) - | NONE => NONE) - | NONE => NONE); - in fun build args_file = Command_Line.tool (fn () =>