# HG changeset patch
# User wenzelm
# Date 1361370142 -3600
# Node ID dff3471dd8bcc84da69e471a1b456fc32485c2bd
# Parent  88c96e836ed6733e002b22358ded890393530341
more tight representation of command timing;
tuned signatures;
tuned;

diff -r 88c96e836ed6 -r dff3471dd8bc src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Wed Feb 20 13:03:50 2013 +0100
+++ b/src/Pure/General/timing.ML	Wed Feb 20 15:22:22 2013 +0100
@@ -16,12 +16,11 @@
 sig
   include BASIC_TIMING
   type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
-  val zero: timing
-  val add: timing -> timing -> timing
   type start
   val start: unit -> start
   val result: start -> timing
   val timing: ('a -> 'b) -> 'a -> timing * 'b
+  val is_relevant_time: Time.time -> bool
   val is_relevant: timing -> bool
   val message: timing -> string
 end
@@ -33,13 +32,6 @@
 
 type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
 
-val zero = {elapsed = Time.zeroTime, cpu = Time.zeroTime, gc = Time.zeroTime};
-
-fun add (t1: timing) (t2: timing) =
- {elapsed = Time.+ (#elapsed t1, #elapsed t2),
-  cpu = Time.+ (#cpu t1, #cpu t2),
-  gc = Time.+ (#gc t1, #gc t2)};
-
 
 (* timer control *)
 
@@ -82,10 +74,12 @@
 
 val min_time = Time.fromMilliseconds 1;
 
+fun is_relevant_time time = Time.>= (time, min_time);
+
 fun is_relevant {elapsed, cpu, gc} =
-  Time.>= (elapsed, min_time) orelse
-  Time.>= (cpu, min_time) orelse
-  Time.>= (gc, min_time);
+  is_relevant_time elapsed orelse
+  is_relevant_time cpu orelse
+  is_relevant_time gc;
 
 fun message {elapsed, cpu, gc} =
   Time.toString elapsed ^ "s elapsed time, " ^
diff -r 88c96e836ed6 -r dff3471dd8bc src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Feb 20 13:03:50 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Feb 20 15:22:22 2013 +0100
@@ -89,9 +89,9 @@
   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 -> Properties.T
-  val get_timing: transition -> Timing.timing
-  val put_timing: Timing.timing -> transition -> transition
+  val approximative_id: transition -> {file: string, offset: int, name: string} option
+  val get_timing: transition -> Time.time
+  val put_timing: Time.time -> transition -> transition
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command: transition -> state -> state
   val proof_result: bool -> transition * transition list -> state ->
@@ -343,7 +343,7 @@
   int_only: bool,            (*interactive-only*)
   print: bool,               (*print result state*)
   no_timing: bool,           (*suppress timing*)
-  timing: Timing.timing,     (*prescient timing information*)
+  timing: Time.time,         (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
 fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
@@ -353,7 +353,7 @@
 fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
   make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
 
-val empty = make_transition ("", Position.none, false, false, false, Timing.zero, []);
+val empty = make_transition ("", Position.none, false, false, false, Time.zeroTime, []);
 
 
 (* diagnostics *)
@@ -591,6 +591,19 @@
 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 =
@@ -614,9 +627,6 @@
 
 (* apply transitions *)
 
-fun approximative_id tr =
-  (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
-
 fun get_timing (Transition {timing, ...}) = timing;
 fun put_timing timing = map_transition (fn (name, pos, int_only, print, no_timing, _, trans) =>
   (name, pos, int_only, print, no_timing, timing, trans));
@@ -624,10 +634,14 @@
 local
 
 fun timing_message tr t =
-  if Timing.is_relevant t andalso not (Position.is_reported (pos_of tr)) then
-    Output.protocol_message
-      (Markup.command_timing :: approximative_id tr @ Markup.timing_properties t) ""
-    handle Fail _ => ()
+  if Timing.is_relevant_time (#elapsed t) andalso not (Position.is_reported (pos_of tr))
+  then
+    (case approximative_id tr of
+      SOME id =>
+        (Output.protocol_message
+          (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
+        handle Fail _ => ())
+    | NONE => ())
   else ();
 
 fun app int (tr as Transition {trans, print, no_timing, ...}) =
@@ -704,9 +718,8 @@
         val (body_trs, end_tr) = split_last proof_trs;
         val finish = Context.Theory o Proof_Context.theory_of;
 
-        val timing_estimate = fold (Timing.add o get_timing) proof_trs Timing.zero;
-        val timing_order =
-          Real.floor (Real.max (Math.log10 (Time.toReal (#elapsed timing_estimate)), ~3.0));
+        val timing_estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
+        val timing_order = Real.floor (Real.max (Math.log10 (Time.toReal timing_estimate), ~3.0));
         val pri = Int.min (timing_order - 3, ~1);
 
         val future_proof = Proof.global_future_proof
diff -r 88c96e836ed6 -r dff3471dd8bc src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Feb 20 13:03:50 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Feb 20 15:22:22 2013 +0100
@@ -95,6 +95,11 @@
   val timing_propertiesN: string list
   val timing_properties: Timing.timing -> Properties.T
   val parse_timing_properties: Properties.T -> Timing.timing
+  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 subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
@@ -352,6 +357,24 @@
   cpu = get_time props cpuN,
   gc = get_time props gcN};
 
+
+(* command timing *)
+
+val command_timingN = "command_timing";
+
+fun command_timing_properties {file, offset, name} elapsed =
+ [(fileN, file), (offsetN, print_int offset),
+  (nameN, name), (elapsedN, Time.toString elapsed)];
+
+fun parse_command_timing_properties props =
+  (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
+    (SOME file, SOME offset, SOME name) =>
+      SOME ({file = file, offset = parse_int offset, name = name}, get_time props elapsedN)
+  | _ => NONE);
+
+
+(* session timing *)
+
 val timingN = "timing";
 fun timing t = (timingN, timing_properties t);
 
diff -r 88c96e836ed6 -r dff3471dd8bc src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Feb 20 13:03:50 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Feb 20 15:22:22 2013 +0100
@@ -17,7 +17,7 @@
   val loaded_files: string -> Path.T list
   val remove_thy: string -> unit
   val kill_thy: string -> unit
-  val use_theories: {last_timing: Toplevel.transition -> Timing.timing, master_dir: Path.T} ->
+  val use_theories: {last_timing: Toplevel.transition -> Time.time, master_dir: Path.T} ->
     (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
@@ -310,7 +310,7 @@
 fun use_theories {last_timing, master_dir} imports =
   schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
 
-val use_thys = use_theories {last_timing = K Timing.zero, master_dir = Path.current};
+val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current};
 val use_thy = use_thys o single;
 
 
@@ -320,7 +320,7 @@
   let
     val {name = (name, _), imports, ...} = header;
     val _ = kill_thy name;
-    val _ = use_theories {last_timing = K Timing.zero, master_dir = master_dir} imports;
+    val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports;
     val _ = Thy_Header.define_keywords header;
     val parents = map (get_theory o base_name o fst) imports;
   in Thy_Load.begin_theory master_dir header parents end;
diff -r 88c96e836ed6 -r dff3471dd8bc src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Feb 20 13:03:50 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Feb 20 15:22:22 2013 +0100
@@ -22,7 +22,7 @@
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
-  val load_thy: (Toplevel.transition -> Timing.timing) -> int -> Path.T -> Thy_Header.header ->
+  val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
     Position.T -> string -> theory list -> theory * unit future
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
diff -r 88c96e836ed6 -r dff3471dd8bc src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Wed Feb 20 13:03:50 2013 +0100
+++ b/src/Pure/Tools/build.ML	Wed Feb 20 15:22:22 2013 +0100
@@ -80,14 +80,29 @@
           " (undefined " ^ commas conds ^ ")\n"))
   end;
 
-structure Timings =
-  Table(type key = Properties.T val ord = dict_ord (prod_ord fast_string_ord fast_string_ord));
+
+(* command timings *)
+
+type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name * time *)
+
+val empty_timings: timings = Symtab.empty;
 
-fun make_timing props =
-  let val (t, id) = List.partition (member (op =) Markup.timing_propertiesN o fst) props
-  in (id, Markup.parse_timing_properties t) end;
+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 make_timings timings = fold (Timings.update o make_timing) timings Timings.empty;
+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 time else Time.zeroTime
+          | NONE => Time.zeroTime)
+      | NONE => Time.zeroTime)
+  | NONE => Time.zeroTime);
 
 in
 
@@ -124,9 +139,7 @@
           (false, "") ""
           verbose;
 
-      val last_timing =
-        the_default Timing.zero o
-          Timings.lookup (make_timings command_timings) o Toplevel.approximative_id;
+      val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
 
       val res1 =
         theories |>