--- 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, " ^
--- 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
--- 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);
--- 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;
--- 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
--- 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 |>