support for prescient timing information within command transactions;

--- a/src/Pure/General/timing.ML	Tue Feb 19 10:55:11 2013 +0100
+++ b/src/Pure/General/timing.ML	Tue Feb 19 12:58:32 2013 +0100
@@ -16,6 +16,8 @@
 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
@@ -27,10 +29,20 @@
 structure Timing: TIMING =
 struct
 
-(* timer control *)
+(* type timing *)
 
 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 *)
+
 abstype start = Start of
   Timer.real_timer * Time.time * Timer.cpu_timer *
     {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}

--- a/src/Pure/Isar/toplevel.ML	Tue Feb 19 10:55:11 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Feb 19 12:58:32 2013 +0100
@@ -89,6 +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 transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command: transition -> state -> state
   val proof_result: bool -> transition * transition list -> state ->
@@ -340,16 +343,17 @@
   int_only: bool,            (*interactive-only*)
   print: bool,               (*print result state*)
   no_timing: bool,           (*suppress timing*)
+  timing: Timing.timing,     (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
-fun make_transition (name, pos, int_only, print, no_timing, trans) =
-  Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing,
-    trans = trans};
+fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
+  Transition {name = name, pos = pos, int_only = int_only, print = print,
+    no_timing = no_timing, timing = timing, trans = trans};
 
-fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) =
-  make_transition (f (name, pos, int_only, print, no_timing, trans));
+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, []);
+val empty = make_transition ("", Position.none, false, false, false, Timing.zero, []);
 
 
 (* diagnostics *)
@@ -367,26 +371,26 @@
 
 (* modify transitions *)
 
-fun name name = map_transition (fn (_, pos, int_only, print, no_timing, trans) =>
-  (name, pos, int_only, print, no_timing, trans));
+fun name name = map_transition (fn (_, pos, int_only, print, no_timing, timing, trans) =>
+  (name, pos, int_only, print, no_timing, timing, trans));
 
-fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) =>
-  (name, pos, int_only, print, no_timing, trans));
+fun position pos = map_transition (fn (name, _, int_only, print, no_timing, timing, trans) =>
+  (name, pos, int_only, print, no_timing, timing, trans));
 
-fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) =>
-  (name, pos, int_only, print, no_timing, trans));
+fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, timing, trans) =>
+  (name, pos, int_only, print, no_timing, timing, trans));
 
-val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
-  (name, pos, int_only, print, true, trans));
+val no_timing = map_transition (fn (name, pos, int_only, print, _, timing, trans) =>
+  (name, pos, int_only, print, true, timing, trans));
 
-fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) =>
-  (name, pos, int_only, print, no_timing, tr :: trans));
+fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, timing, trans) =>
+  (name, pos, int_only, print, no_timing, timing, tr :: trans));
 
-val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) =>
-  (name, pos, int_only, print, no_timing, []));
+val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, timing, _) =>
+  (name, pos, int_only, print, no_timing, timing, []));
 
-fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, trans) =>
-  (name, pos, int_only, print, no_timing, trans));
+fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, timing, trans) =>
+  (name, pos, int_only, print, no_timing, timing, trans));
 
 val print = set_print true;
 
@@ -610,13 +614,19 @@
 
 (* 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));
+
 local
 
 fun timing_message tr t =
   if Timing.is_relevant t then
     Output.protocol_message
-      (Markup.command_timing :: (Markup.nameN, name_of tr) ::
-        Position.properties_of (pos_of tr) @ Markup.timing_properties t) ""
+      (Markup.command_timing :: approximative_id tr @ Markup.timing_properties t) ""
     handle Fail _ => ()
   else ();
 

--- a/src/Pure/PIDE/markup.ML	Tue Feb 19 10:55:11 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Feb 19 12:58:32 2013 +0100
@@ -92,6 +92,7 @@
   val elapsedN: string
   val cpuN: string
   val gcN: string
+  val timing_propertiesN: string list
   val timing_properties: Timing.timing -> Properties.T
   val timingN: string val timing: Timing.timing -> T
   val subgoalsN: string
@@ -333,6 +334,8 @@
 val cpuN = "cpu";
 val gcN = "gc";
 
+val timing_propertiesN = [elapsedN, cpuN, gcN];
+
 fun timing_properties {elapsed, cpu, gc} =
  [(elapsedN, Time.toString elapsed),
   (cpuN, Time.toString cpu),

--- a/src/Pure/Thy/thy_info.ML	Tue Feb 19 10:55:11 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Tue Feb 19 12:58:32 2013 +0100
@@ -17,7 +17,8 @@
   val loaded_files: string -> Path.T list
   val remove_thy: string -> unit
   val kill_thy: string -> unit
-  val use_thys_wrt: Path.T -> (string * Position.T) list -> unit
+  val use_theories: {last_timing: Toplevel.transition -> Timing.timing, master_dir: Path.T} ->
+    (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
   val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
@@ -221,7 +222,7 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy initiators update_time deps text (name, pos) uses keywords parents =
+fun load_thy last_timing initiators update_time deps text (name, pos) uses keywords parents =
   let
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -234,7 +235,7 @@
     val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
 
     val (theory, present) =
-      Thy_Load.load_thy update_time dir header (Path.position thy_path) text
+      Thy_Load.load_thy last_timing update_time dir header (Path.position thy_path) text
         (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
   in (theory, present, commit) end;
@@ -259,9 +260,9 @@
 
 in
 
-fun require_thys initiators dir strs tasks =
-      fold_map (require_thy initiators dir) strs tasks |>> forall I
-and require_thy initiators dir (str, require_pos) tasks =
+fun require_thys last_timing initiators dir strs tasks =
+      fold_map (require_thy last_timing initiators dir) strs tasks |>> forall I
+and require_thy last_timing initiators dir (str, require_pos) tasks =
   let
     val path = Path.expand (Path.explode str);
     val name = Path.implode (Path.base path);
@@ -280,7 +281,7 @@
 
           val parents = map (base_name o #1) imports;
           val (parents_current, tasks') =
-            require_thys (name :: initiators)
+            require_thys last_timing (name :: initiators)
               (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
@@ -293,7 +294,8 @@
                   let
                     val update_time = serial ();
                     val load =
-                      load_thy initiators update_time dep text (name, theory_pos) uses keywords;
+                      load_thy last_timing initiators update_time dep
+                        text (name, theory_pos) uses keywords;
                   in Task (parents, load) end);
 
           val tasks'' = new_entry name parents task tasks';
@@ -305,10 +307,10 @@
 
 (* use_thy *)
 
-fun use_thys_wrt dir arg =
-  schedule_tasks (snd (require_thys [] dir arg String_Graph.empty));
+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_thys_wrt Path.current;
+val use_thys = use_theories {last_timing = K Timing.zero, master_dir = Path.current};
 val use_thy = use_thys o single;
 
 
@@ -318,7 +320,7 @@
   let
     val {name = (name, _), imports, ...} = header;
     val _ = kill_thy name;
-    val _ = use_thys_wrt master_dir imports;
+    val _ = use_theories {last_timing = K Timing.zero, 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;

--- a/src/Pure/Thy/thy_load.ML	Tue Feb 19 10:55:11 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Tue Feb 19 12:58:32 2013 +0100
@@ -22,8 +22,8 @@
   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: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
-    theory list -> theory * unit future
+  val load_thy: (Toplevel.transition -> Timing.timing) -> 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
 end;
@@ -214,10 +214,13 @@
   |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   |> Theory.checkpoint;
 
-fun excursion init elements =
+fun excursion last_timing init elements =
   let
     val immediate = not (Goal.future_enabled ());
 
+    fun put_timing tr = Toplevel.put_timing (last_timing tr) tr;
+    fun put_timings (tr, trs) = (put_timing tr, map put_timing trs);
+
     fun proof_result (tr, trs) (st, _) =
       let
         val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
@@ -225,7 +228,7 @@
       in (result, (st', pos')) end;
 
     fun element_result elem x =
-      fold_map proof_result
+      fold_map (proof_result o put_timings)
         (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
 
     val (results, (end_state, end_pos)) =
@@ -234,7 +237,7 @@
     val thy = Toplevel.end_theory end_pos end_state;
   in (flat results, thy) end;
 
-fun load_thy update_time master_dir header text_pos text parents =
+fun load_thy last_timing update_time master_dir header text_pos text parents =
   let
     val time = ! Toplevel.timing;
 
@@ -255,7 +258,7 @@
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
-    val (results, thy) = cond_timeit time "" (fn () => excursion init elements);
+    val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
     val present =

--- a/src/Pure/Tools/build.ML	Tue Feb 19 10:55:11 2013 +0100
+++ b/src/Pure/Tools/build.ML	Tue Feb 19 12:58:32 2013 +0100
@@ -44,8 +44,8 @@
 fun no_document options =
   (case Options.string options "document" of "" => true | "false" => true | _ => false);
 
-fun use_thys options =
-  Thy_Info.use_thys
+fun use_theories last_timing options =
+  Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
     |> Unsynchronized.setmp print_mode
         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
@@ -71,10 +71,10 @@
     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
 
-fun use_theories (options, thys) =
+fun use_theories_condition last_timing (options, thys) =
   let val condition = space_explode "," (Options.string options "condition") in
     (case filter_out (can getenv_strict) condition of
-      [] => use_thys options (map (rpair Position.none) thys)
+      [] => use_theories last_timing options (map (rpair Position.none) thys)
     | conds =>
         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
           " (undefined " ^ commas conds ^ ")\n"))
@@ -117,7 +117,7 @@
 
       val res1 =
         theories |>
-          (List.app use_theories
+          (List.app (use_theories_condition (K Timing.zero))  (* FIXME *)
             |> Session.with_timing name verbose
             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")