just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
authorwenzelm
Tue Apr 09 20:16:52 2013 +0200 (2013-04-09 ago)
changeset 516623391a493f39a
parent 51661 92e58b76dbb1
child 51663 098f3cf6c809
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
src/Pure/General/timing.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/markup.scala
src/Pure/System/isar.ML
src/Pure/System/session.scala
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/General/timing.ML	Tue Apr 09 15:59:02 2013 +0200
     1.2 +++ b/src/Pure/General/timing.ML	Tue Apr 09 20:16:52 2013 +0200
     1.3 @@ -23,7 +23,8 @@
     1.4    val is_relevant_time: Time.time -> bool
     1.5    val is_relevant: timing -> bool
     1.6    val message: timing -> string
     1.7 -  val status: ('a -> 'b) -> 'a -> 'b
     1.8 +  val protocol_message: Properties.T -> timing -> unit
     1.9 +  val protocol: Properties.T -> ('a -> 'b) -> 'a -> 'b
    1.10  end
    1.11  
    1.12  structure Timing: TIMING =
    1.13 @@ -103,10 +104,13 @@
    1.14  fun timeap f x = timeit (fn () => f x);
    1.15  fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
    1.16  
    1.17 -fun status f x =
    1.18 +fun protocol_message props t =
    1.19 +  Output.try_protocol_message (props @ Markup.timing_properties t) "";
    1.20 +
    1.21 +fun protocol props f x =
    1.22    let
    1.23      val (t, result) = timing (Exn.interruptible_capture f) x;
    1.24 -    val _ = if is_relevant t then Output.status (Markup.markup_only (Markup.timing t)) else ();
    1.25 +    val _ = protocol_message props t;
    1.26    in Exn.release result end;
    1.27  
    1.28  end;
     2.1 --- a/src/Pure/Isar/proof.ML	Tue Apr 09 15:59:02 2013 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Tue Apr 09 20:16:52 2013 +0200
     2.3 @@ -1154,16 +1154,20 @@
     2.4  end;
     2.5  
     2.6  
     2.7 -(* terminal proofs *)
     2.8 +(* terminal proofs *)  (* FIXME avoid toplevel imitation -- include in PIDE/document *)
     2.9  
    2.10  local
    2.11  
    2.12  fun future_terminal_proof proof1 proof2 done int state =
    2.13    if Goal.future_enabled_level 3 andalso not (is_relevant state) then
    2.14      state |> future_proof (fn state' =>
    2.15 -      Goal.fork_params
    2.16 -        {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
    2.17 -        (fn () => ((), Timing.status proof2 state'))) |> snd |> done
    2.18 +      let
    2.19 +        val pos = Position.thread_data ();
    2.20 +        val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos;
    2.21 +      in
    2.22 +        Goal.fork_params {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
    2.23 +          (fn () => ((), Timing.protocol props proof2 state'))
    2.24 +      end) |> snd |> done
    2.25    else proof1 state;
    2.26  
    2.27  in
     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Apr 09 15:59:02 2013 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Apr 09 20:16:52 2013 +0200
     3.3 @@ -89,7 +89,6 @@
     3.4    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
     3.5    val status: transition -> Markup.T -> unit
     3.6    val add_hook: (transition -> state -> state -> unit) -> unit
     3.7 -  val approximative_id: transition -> {file: string, offset: int, name: string} option
     3.8    val get_timing: transition -> Time.time option
     3.9    val put_timing: Time.time option -> transition -> transition
    3.10    val transition: bool -> transition -> state -> (state * (exn * string) option) option
    3.11 @@ -591,19 +590,6 @@
    3.12  fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
    3.13  
    3.14  
    3.15 -(* approximative identification within source file *)
    3.16 -
    3.17 -fun approximative_id tr =
    3.18 -  let
    3.19 -    val name = name_of tr;
    3.20 -    val pos = pos_of tr;
    3.21 -  in
    3.22 -    (case (Position.file_of pos, Position.offset_of pos) of
    3.23 -      (SOME file, SOME offset) => SOME {file = file, offset = offset, name = name}
    3.24 -    | _ => NONE)
    3.25 -  end;
    3.26 -
    3.27 -
    3.28  (* thread position *)
    3.29  
    3.30  fun setmp_thread_position (Transition {pos, ...}) f x =
    3.31 @@ -643,23 +629,9 @@
    3.32        val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
    3.33  
    3.34        val timing_result = Timing.result timing_start;
    3.35 -
    3.36 -      val _ =
    3.37 -        if Timing.is_relevant timing_result andalso (! profiling > 0 orelse ! timing)
    3.38 -          andalso not (Keyword.is_control (name_of tr))
    3.39 -        then tracing (command_msg "" tr ^ ": " ^ Timing.message timing_result)
    3.40 -        else ();
    3.41 -      val _ =
    3.42 -        if Timing.is_relevant timing_result
    3.43 -        then status tr (Markup.timing timing_result)
    3.44 -        else ();
    3.45 -      val _ =
    3.46 -        (case approximative_id tr of
    3.47 -          SOME id =>
    3.48 -            (Output.try_protocol_message
    3.49 -              (Markup.command_timing ::
    3.50 -                Markup.command_timing_properties id (#elapsed timing_result)) "")
    3.51 -        | NONE => ());
    3.52 +      val timing_props =
    3.53 +        Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
    3.54 +      val _ = Timing.protocol_message timing_props timing_result;
    3.55      in
    3.56        (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err)
    3.57      end);
     4.1 --- a/src/Pure/PIDE/markup.scala	Tue Apr 09 15:59:02 2013 +0200
     4.2 +++ b/src/Pure/PIDE/markup.scala	Tue Apr 09 20:16:52 2013 +0200
     4.3 @@ -193,6 +193,7 @@
     4.4    {
     4.5      def apply(timing: isabelle.Timing): Properties.T =
     4.6        Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
     4.7 +
     4.8      def unapply(props: Properties.T): Option[isabelle.Timing] =
     4.9        (props, props, props) match {
    4.10          case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
    4.11 @@ -206,6 +207,7 @@
    4.12    object Timing
    4.13    {
    4.14      def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
    4.15 +
    4.16      def unapply(markup: Markup): Option[isabelle.Timing] =
    4.17        markup match {
    4.18          case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
    4.19 @@ -214,6 +216,22 @@
    4.20    }
    4.21  
    4.22  
    4.23 +  /* command timing */
    4.24 +
    4.25 +  object Command_Timing
    4.26 +  {
    4.27 +    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
    4.28 +      props match {
    4.29 +        case (FUNCTION, "command_timing") :: args =>
    4.30 +          (args, args) match {
    4.31 +            case (Position.Id(id), Timing_Properties(timing)) => Some((id, timing))
    4.32 +            case _ => None
    4.33 +          }
    4.34 +        case _ => None
    4.35 +      }
    4.36 +  }
    4.37 +
    4.38 +
    4.39    /* toplevel */
    4.40  
    4.41    val SUBGOALS = "subgoals"
     5.1 --- a/src/Pure/System/isar.ML	Tue Apr 09 15:59:02 2013 +0200
     5.2 +++ b/src/Pure/System/isar.ML	Tue Apr 09 20:16:52 2013 +0200
     5.3 @@ -118,6 +118,23 @@
     5.4  
     5.5  local
     5.6  
     5.7 +fun protocol_message props output =
     5.8 +  (case props of
     5.9 +    function :: args =>
    5.10 +      if function = Markup.command_timing then
    5.11 +        let
    5.12 +          val name = the_default "" (Properties.get args Markup.nameN);
    5.13 +          val pos = Position.of_properties args;
    5.14 +          val timing = Markup.parse_timing_properties args;
    5.15 +        in
    5.16 +          if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing)
    5.17 +            andalso name <> "" andalso not (Keyword.is_control name)
    5.18 +          then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing)
    5.19 +          else ()
    5.20 +        end
    5.21 +      else raise Output.Protocol_Message props
    5.22 +  | [] => raise Output.Protocol_Message props);
    5.23 +
    5.24  fun raw_loop secure src =
    5.25    let
    5.26      fun check_secure () =
    5.27 @@ -139,6 +156,7 @@
    5.28  fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
    5.29   (Context.set_thread_data NONE;
    5.30    if do_init then (Options.load_default (); init ()) else ();
    5.31 +  Output.Private_Hooks.protocol_message_fn := protocol_message;
    5.32    if welcome then writeln (Session.welcome ()) else ();
    5.33    uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
    5.34  
     6.1 --- a/src/Pure/System/session.scala	Tue Apr 09 15:59:02 2013 +0200
     6.2 +++ b/src/Pure/System/session.scala	Tue Apr 09 20:16:52 2013 +0200
     6.3 @@ -300,22 +300,31 @@
     6.4      def handle_output(output: Isabelle_Process.Output)
     6.5      //{{{
     6.6      {
     6.7 -      def bad_output(output: Isabelle_Process.Output)
     6.8 +      def bad_output()
     6.9        {
    6.10          if (verbose)
    6.11            System.err.println("Ignoring prover output: " + output.message.toString)
    6.12        }
    6.13  
    6.14 +      def accumulate(state_id: Document.ID, message: XML.Elem)
    6.15 +      {
    6.16 +        try {
    6.17 +          val st = global_state >>> (_.accumulate(state_id, message))
    6.18 +          delay_commands_changed.invoke(false, List(st.command))
    6.19 +        }
    6.20 +        catch {
    6.21 +          case _: Document.State.Fail => bad_output()
    6.22 +        }
    6.23 +      }
    6.24 +
    6.25        output.properties match {
    6.26  
    6.27          case Position.Id(state_id) if !output.is_protocol =>
    6.28 -          try {
    6.29 -            val st = global_state >>> (_.accumulate(state_id, output.message))
    6.30 -            delay_commands_changed.invoke(false, List(st.command))
    6.31 -          }
    6.32 -          catch {
    6.33 -            case _: Document.State.Fail => bad_output(output)
    6.34 -          }
    6.35 +          accumulate(state_id, output.message)
    6.36 +
    6.37 +        case Markup.Command_Timing(state_id, timing) if output.is_protocol =>
    6.38 +          // FIXME XML.cache (!?)
    6.39 +          accumulate(state_id, XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))))
    6.40  
    6.41          case Markup.Assign_Execs if output.is_protocol =>
    6.42            XML.content(output.body) match {
    6.43 @@ -324,8 +333,8 @@
    6.44                  val cmds = global_state >>> (_.assign(id, assign))
    6.45                  delay_commands_changed.invoke(true, cmds)
    6.46                }
    6.47 -              catch { case _: Document.State.Fail => bad_output(output) }
    6.48 -            case _ => bad_output(output)
    6.49 +              catch { case _: Document.State.Fail => bad_output() }
    6.50 +            case _ => bad_output()
    6.51            }
    6.52            // FIXME separate timeout event/message!?
    6.53            if (prover.isDefined && System.currentTimeMillis() > prune_next) {
    6.54 @@ -340,8 +349,8 @@
    6.55                try {
    6.56                  global_state >> (_.removed_versions(removed))
    6.57                }
    6.58 -              catch { case _: Document.State.Fail => bad_output(output) }
    6.59 -            case _ => bad_output(output)
    6.60 +              catch { case _: Document.State.Fail => bad_output() }
    6.61 +            case _ => bad_output()
    6.62            }
    6.63  
    6.64          case Markup.Invoke_Scala(name, id) if output.is_protocol =>
    6.65 @@ -374,7 +383,7 @@
    6.66            if (rc == 0) phase = Session.Inactive
    6.67            else phase = Session.Failed
    6.68  
    6.69 -        case _ => bad_output(output)
    6.70 +        case _ => bad_output()
    6.71        }
    6.72      }
    6.73      //}}}
     7.1 --- a/src/Pure/Tools/build.ML	Tue Apr 09 15:59:02 2013 +0200
     7.2 +++ b/src/Pure/Tools/build.ML	Tue Apr 09 20:16:52 2013 +0200
     7.3 @@ -12,16 +12,56 @@
     7.4  structure Build: BUILD =
     7.5  struct
     7.6  
     7.7 +(* command timings *)
     7.8 +
     7.9 +type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name * time *)
    7.10 +
    7.11 +val empty_timings: timings = Symtab.empty;
    7.12 +
    7.13 +fun update_timings props =
    7.14 +  (case Markup.parse_command_timing_properties props of
    7.15 +    SOME ({file, offset, name}, time) =>
    7.16 +      Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
    7.17 +  | NONE => I);
    7.18 +
    7.19 +fun approximative_id name pos =
    7.20 +  (case (Position.file_of pos, Position.offset_of pos) of
    7.21 +    (SOME file, SOME offset) =>
    7.22 +      if name = "" then NONE else SOME {file = file, offset = offset, name = name}
    7.23 +  | _ => NONE);
    7.24 +
    7.25 +fun lookup_timings timings tr =
    7.26 +  (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
    7.27 +    SOME {file, offset, name} =>
    7.28 +      (case Symtab.lookup timings file of
    7.29 +        SOME offsets =>
    7.30 +          (case Inttab.lookup offsets offset of
    7.31 +            SOME (name', time) => if name = name' then SOME time else NONE
    7.32 +          | NONE => NONE)
    7.33 +      | NONE => NONE)
    7.34 +  | NONE => NONE);
    7.35 +
    7.36 +
    7.37  (* protocol messages *)
    7.38  
    7.39 -(* FIXME avoid hardwired stuff!? *)
    7.40 -val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
    7.41 +fun inline_message a args =
    7.42 +  writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
    7.43  
    7.44  fun protocol_message props output =
    7.45    (case props of
    7.46      function :: args =>
    7.47 -      if member (op =) protocol_echo function then
    7.48 -        writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
    7.49 +      if function = Markup.ML_statistics orelse function = Markup.task_statistics then
    7.50 +        inline_message (#2 function) args
    7.51 +      else if function = Markup.command_timing then
    7.52 +        let
    7.53 +          val name = the_default "" (Properties.get args Markup.nameN);
    7.54 +          val pos = Position.of_properties args;
    7.55 +          val {elapsed, ...} = Markup.parse_timing_properties args;
    7.56 +        in
    7.57 +          (case approximative_id name pos of
    7.58 +            SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
    7.59 +          | NONE => ())
    7.60 +        end
    7.61        else
    7.62          (case Markup.dest_loading_theory props of
    7.63            SOME name => writeln ("\floading_theory = " ^ name)
    7.64 @@ -74,30 +114,6 @@
    7.65            " (undefined " ^ commas conds ^ ")\n"))
    7.66    end;
    7.67  
    7.68 -
    7.69 -(* command timings *)
    7.70 -
    7.71 -type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name * time *)
    7.72 -
    7.73 -val empty_timings: timings = Symtab.empty;
    7.74 -
    7.75 -fun update_timings props =
    7.76 -  (case Markup.parse_command_timing_properties props of
    7.77 -    SOME ({file, offset, name}, time) =>
    7.78 -      Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
    7.79 -  | NONE => I);
    7.80 -
    7.81 -fun lookup_timings timings tr =
    7.82 -  (case Toplevel.approximative_id tr of
    7.83 -    SOME {file, offset, name} =>
    7.84 -      (case Symtab.lookup timings file of
    7.85 -        SOME offsets =>
    7.86 -          (case Inttab.lookup offsets offset of
    7.87 -            SOME (name', time) => if name = name' then SOME time else NONE
    7.88 -          | NONE => NONE)
    7.89 -      | NONE => NONE)
    7.90 -  | NONE => NONE);
    7.91 -
    7.92  in
    7.93  
    7.94  fun build args_file = Command_Line.tool (fn () =>