# HG changeset patch
# User wenzelm
# Date 1361455804 -3600
# Node ID 67882f99274e2d2ed598e83ec5e5186b2e676624
# Parent  9ee38fc0bc811f4a4d120822c2daad2fa74f62e8# Parent  19192615911ecb3958099998f83e292abf69d891
merged

diff -r 9ee38fc0bc81 -r 67882f99274e etc/options
--- a/etc/options	Thu Feb 21 12:22:26 2013 +0100
+++ b/etc/options	Thu Feb 21 15:10:04 2013 +0100
@@ -53,6 +53,8 @@
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_proofs_threshold : int = 100
   -- "threshold for sub-proof parallelization"
+option parallel_proofs_reuse_timing : bool = true
+  -- "reuse timing information from old log file for parallel proof scheduling"
 
 
 section "Detail of Proof Recording"
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/General/timing.ML	Thu Feb 21 15:10:04 2013 +0100
@@ -20,6 +20,7 @@
   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
@@ -27,10 +28,13 @@
 structure Timing: TIMING =
 struct
 
-(* timer control *)
+(* type timing *)
 
 type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
 
+
+(* 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}}
@@ -70,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 9ee38fc0bc81 -r 67882f99274e src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Feb 21 15:10:04 2013 +0100
@@ -63,6 +63,7 @@
   val is_theory_load: string -> bool
   val is_theory: string -> bool
   val is_proof: string -> bool
+  val is_proof_body: string -> bool
   val is_theory_goal: string -> bool
   val is_proof_goal: string -> bool
   val is_schematic_goal: string -> bool
@@ -230,10 +231,13 @@
 
 (* command categories *)
 
-fun command_category ks name =
-  (case command_keyword name of
-    NONE => false
-  | SOME k => member (op = o pairself kind_of) ks k);
+fun command_category ks =
+  let val tab = Symtab.make_set (map kind_of ks) in
+    fn name =>
+      (case command_keyword name of
+        NONE => false
+      | SOME k => Symtab.defined tab (kind_of k))
+  end;
 
 val is_diag = command_category [diag];
 val is_control = command_category [control];
@@ -256,6 +260,10 @@
     prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
     prf_asm, prf_asm_goal, prf_script];
 
+val is_proof_body = command_category
+  [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+
 val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal];
 val is_schematic_goal = command_category [thy_schematic_goal];
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Feb 21 15:10:04 2013 +0100
@@ -36,7 +36,7 @@
   val isar: TextIO.instream -> bool -> isar
   val span_cmts: Token.T list -> Token.T list
   val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
-  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
+  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
 end;
 
@@ -331,13 +331,16 @@
       handle ERROR msg => (Toplevel.malformed proper_range msg, true)
   end;
 
-fun read_element outer_syntax init {head, proof, proper_proof} =
+fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) =
   let
     val read = read_span outer_syntax o Thy_Syntax.span_content;
     val (tr, proper_head) = read head |>> Toplevel.modify_init init;
-    val proof_trs = map read proof |> filter #2 |> map #1;
+    val proof_trs =
+      (case opt_proof of
+        NONE => []
+      | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1);
   in
-    if proper_head andalso proper_proof andalso
+    if proper_head andalso
       not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   end;
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Feb 21 15:10:04 2013 +0100
@@ -114,6 +114,7 @@
   val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
+  val is_relevant: state -> bool
   val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
   val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
   val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
@@ -1188,7 +1189,7 @@
     andalso not (is_relevant state)
   then
     snd (proof2 (fn state' =>
-      Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state)
+      Goal.fork_name "Proof.future_terminal_proof" ~1 (fn () => ((), proof1 meths state'))) state)
   else proof1 meths state;
 
 in
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Feb 21 15:10:04 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 -> {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 ->
@@ -340,16 +343,17 @@
   int_only: bool,            (*interactive-only*)
   print: bool,               (*print result state*)
   no_timing: bool,           (*suppress timing*)
+  timing: Time.time,         (*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, Time.zeroTime, []);
 
 
 (* 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;
 
@@ -587,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 =
@@ -610,14 +627,31 @@
 
 (* apply transitions *)
 
+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_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, ...}) =
   setmp_thread_position tr (fn state =>
     let
       fun do_timing f x = (warning (command_msg "" tr); timeap f x);
       fun do_profiling f x = profile (! profiling) f x;
 
+      val start = Timing.start ();
+
       val (result, status) =
          state |>
           (apply_trans int trans
@@ -625,6 +659,8 @@
             |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
 
       val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
+
+      val _ = timing_message tr (Timing.result start);
     in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
 
 in
@@ -672,7 +708,8 @@
 
 fun proof_result immediate (tr, proof_trs) st =
   let val st' = command tr st in
-    if immediate orelse null proof_trs orelse not (can proof_of st')
+    if immediate orelse null proof_trs orelse not (can proof_of st') orelse
+      Proof.is_relevant (proof_of st')
     then
       let val (results, st'') = fold_map command_result proof_trs st'
       in (Future.value ((tr, st') :: results), st'') end
@@ -681,9 +718,13 @@
         val (body_trs, end_tr) = split_last proof_trs;
         val finish = Context.Theory o Proof_Context.theory_of;
 
+        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
           (fn prf =>
-            Goal.fork_name "Toplevel.future_proof"
+            Goal.fork_name "Toplevel.future_proof" pri
               (fn () =>
                 let val (result, result_state) =
                   (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Feb 21 15:10:04 2013 +0100
@@ -92,7 +92,14 @@
   val elapsedN: string
   val cpuN: string
   val gcN: string
+  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
@@ -135,6 +142,7 @@
   val cancel_scala: string -> Properties.T
   val ML_statistics: Properties.entry
   val task_statistics: Properties.entry
+  val command_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val no_output: Output.output * Output.output
@@ -332,11 +340,41 @@
 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),
   (gcN, Time.toString gc)];
 
+fun get_time props name =
+  (case AList.lookup (op =) props name of
+    NONE => Time.zeroTime
+  | SOME s => seconds (the_default 0.0 (Real.fromString s)));
+
+fun parse_timing_properties props =
+ {elapsed = get_time props elapsedN,
+  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);
 
@@ -415,6 +453,8 @@
 
 val task_statistics = (functionN, "task_statistics");
 
+val command_timing = (functionN, "command_timing");
+
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/PIDE/xml.scala	Thu Feb 21 15:10:04 2013 +0100
@@ -188,6 +188,7 @@
 
     // main methods
     def cache_string(x: String): String = synchronized { _cache_string(x) }
+    def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
     def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
     def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
     def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Pure.thy	Thu Feb 21 15:10:04 2013 +0100
@@ -41,8 +41,8 @@
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
   and "context" "locale" :: thy_decl
-  and "sublocale" "interpretation" :: thy_schematic_goal
-  and "interpret" :: prf_goal % "proof"  (* FIXME schematic? *)
+  and "sublocale" "interpretation" :: thy_goal
+  and "interpret" :: prf_goal % "proof"
   and "class" :: thy_decl
   and "subclass" :: thy_goal
   and "instantiation" :: thy_decl
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Feb 21 15:10:04 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 -> 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
   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 Time.zeroTime, 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 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 9ee38fc0bc81 -r 67882f99274e src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Thu Feb 21 15:10:04 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 -> 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
 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 =
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Thu Feb 21 15:10:04 2013 +0100
@@ -15,8 +15,10 @@
   val span_content: span -> Token.T list
   val present_span: span -> Output.output
   val parse_spans: Token.T list -> span list
-  type element = {head: span, proof: span list, proper_proof: bool}
-  val parse_elements: span list -> element list
+  datatype 'a element = Element of 'a * ('a element list * 'a) option
+  val map_element: ('a -> 'b) -> 'a element -> 'b element
+  val flat_element: 'a element -> 'a list
+  val parse_elements: span list -> span element list
 end;
 
 structure Thy_Syntax: THY_SYNTAX =
@@ -134,10 +136,17 @@
 
 (** specification elements: commands with optional proof **)
 
-type element = {head: span, proof: span list, proper_proof: bool};
+datatype 'a element = Element of 'a * ('a element list * 'a) option;
+
+fun element (a, b) = Element (a, SOME b);
+fun atom a = Element (a, NONE);
 
-fun make_element head proof proper_proof =
-  {head = head, proof = proof, proper_proof = proper_proof};
+fun map_element f (Element (a, NONE)) = Element (f a, NONE)
+  | map_element f (Element (a, SOME (elems, b))) =
+      Element (f a, SOME ((map o map_element) f elems, f b));
+
+fun flat_element (Element (a, NONE)) = [a]
+  | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
 
 
 (* scanning spans *)
@@ -159,24 +168,21 @@
 fun command_with pred =
   Scan.one (fn (Span (Command (name, _), _)) => pred name | _ => false);
 
-val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
-  if d <= 0 then Scan.fail
-  else
-    command_with Keyword.is_qed_global >> pair ~1 ||
-    command_with Keyword.is_proof_goal >> pair (d + 1) ||
-    (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
-    Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
+val proof_atom =
+  Scan.one (fn (Span (Command (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
 
-val element =
-  command_with Keyword.is_theory_goal -- proof
-    >> (fn (a, (bs, d)) => make_element a bs (d >= 0)) ||
-  Scan.one not_eof >> (fn a => make_element a [] true);
+fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
+and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
+
+val other_element =
+  command_with Keyword.is_theory_goal -- proof_rest >> element ||
+  Scan.one not_eof >> atom;
 
 in
 
 val parse_elements =
   Source.of_list #>
-  Source.source stopper (Scan.bulk element) NONE #>
+  Source.source stopper (Scan.bulk other_element) NONE #>
   Source.exhaust;
 
 end;
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Tools/build.ML	Thu Feb 21 15:10:04 2013 +0100
@@ -16,30 +16,23 @@
 
 local
 
-fun ML_statistics (function :: stats) "" =
-      if function = Markup.ML_statistics then SOME stats
-      else NONE
-  | ML_statistics _ _ = NONE;
+(* FIXME avoid hardwired stuff!? *)
+val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
 
-fun task_statistics (function :: stats) "" =
-      if function = Markup.task_statistics then SOME stats
-      else NONE
-  | task_statistics _ _ = NONE;
-
-val print_properties = YXML.string_of_body o XML.Encode.properties;
+fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
 
 in
 
 fun protocol_message props output =
-  (case ML_statistics props output of
-    SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
-  | NONE =>
-      (case task_statistics props output of
-        SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
-      | NONE =>
-          (case Markup.dest_loading_theory props of
-            SOME name => writeln ("\floading_theory = " ^ name)
-          | NONE => raise Fail "Undefined Output.protocol_message")));
+  (case props of
+    function :: args =>
+      if member (op =) protocol_echo function then
+        writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
+      else
+        (case Markup.dest_loading_theory props of
+          SOME name => writeln ("\floading_theory = " ^ name)
+        | NONE => protocol_undef ())
+  | [] => protocol_undef ());
 
 end;
 
@@ -51,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 ())
@@ -78,25 +71,49 @@
     |> 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"))
   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 time else Time.zeroTime
+          | NONE => Time.zeroTime)
+      | NONE => Time.zeroTime)
+  | NONE => Time.zeroTime);
+
 in
 
 fun build args_file = Command_Line.tool (fn () =>
     let
-      val (do_output, (options, (verbose, (browser_info, (parent_name,
-          (name, theories)))))) =
+      val (command_timings, (do_output, (options, (verbose, (browser_info,
+          (parent_name, (name, theories))))))) =
         File.read (Path.explode args_file) |> YXML.parse_body |>
           let open XML.Decode in
-            pair bool (pair Options.decode (pair bool (pair string (pair string
-              (pair string ((list (pair Options.decode (list string)))))))))
+            pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
+              (pair string (pair string ((list (pair Options.decode (list string))))))))))
           end;
 
       val document_variants =
@@ -122,9 +139,11 @@
           (false, "") ""
           verbose;
 
+      val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
+
       val res1 =
         theories |>
-          (List.app use_theories
+          (List.app (use_theories_condition last_timing)
             |> Session.with_timing name verbose
             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/Tools/build.scala	Thu Feb 21 15:10:04 2013 +0100
@@ -288,41 +288,71 @@
 
   object Queue
   {
-    def apply(tree: Session_Tree): Queue =
+    def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
     {
       val graph = tree.graph
+      val sessions = graph.keys.toList
+
+      val timings = sessions.map((name: String) =>
+        if (tree(name).options.bool("parallel_proofs_reuse_timing")) (name, load_timings(name))
+        else (name, (Nil, 0.0)))
+      val command_timings =
+        Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
+      val session_timing =
+        Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
 
       def outdegree(name: String): Int = graph.imm_succs(name).size
       def timeout(name: String): Double = tree(name).options.real("timeout")
 
       object Ordering extends scala.math.Ordering[String]
       {
+        def compare_timing(name1: String, name2: String): Int =
+        {
+          val t1 = session_timing(name1)
+          val t2 = session_timing(name2)
+          if (t1 == 0.0 || t2 == 0.0) 0
+          else t1 compare t2
+        }
+
         def compare(name1: String, name2: String): Int =
           outdegree(name2) compare outdegree(name1) match {
             case 0 =>
-              timeout(name2) compare timeout(name1) match {
-                case 0 => name1 compare name2
+              compare_timing(name2, name1) match {
+                case 0 =>
+                  timeout(name2) compare timeout(name1) match {
+                    case 0 => name1 compare name2
+                    case ord => ord
+                  }
                 case ord => ord
               }
             case ord => ord
           }
       }
 
-      new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
+      new Queue(graph, SortedSet(sessions: _*)(Ordering), command_timings)
     }
   }
 
-  final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
+  final class Queue private(
+    graph: Graph[String, Session_Info],
+    order: SortedSet[String],
+    val command_timings: String => List[Properties.T])
   {
     def is_inner(name: String): Boolean = !graph.is_maximal(name)
 
     def is_empty: Boolean = graph.is_empty
 
-    def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
+    def - (name: String): Queue =
+      new Queue(graph.del_node(name),
+        order - name,  // FIXME scala-2.10.0 TreeSet problem!?
+        command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
     {
-      val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
+      val it = order.iterator.dropWhile(name =>
+        skip(name)
+          || !graph.defined(name)  // FIXME scala-2.10.0 TreeSet problem!?
+          || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
       else None
     }
@@ -419,7 +449,7 @@
 
   private class Job(progress: Build.Progress,
     name: String, val info: Session_Info, output: Path, do_output: Boolean,
-    verbose: Boolean, browser_info: Path)
+    verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
   {
     // global browser info dir
     if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
@@ -443,10 +473,10 @@
       else
         {
           import XML.Encode._
-              pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
-                pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
-              (do_output, (info.options, (verbose, (browser_info, (parent,
-                (name, info.theories)))))))
+              pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
+                pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+              (command_timings, (do_output, (info.options, (verbose, (browser_info,
+                (parent, (name, info.theories))))))))
         }))
 
     private val env =
@@ -546,17 +576,26 @@
 
 
   sealed case class Log_Info(
-    name: String, stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
+    name: String,
+    stats: List[Properties.T],
+    tasks: List[Properties.T],
+    command_timings: List[Properties.T],
+    session_timing: Properties.T)
 
-  def parse_log(text: String): Log_Info =
+  def parse_log(full_stats: Boolean, text: String): Log_Info =
   {
     val lines = split_lines(text)
+    val xml_cache = new XML.Cache()
+    def parse_lines(prfx: String): List[Properties.T] =
+      Props.parse_lines(prfx, lines).map(xml_cache.cache_props)
+
     val name =
       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
-    val stats = Props.parse_lines("\fML_statistics = ", lines)
-    val tasks = Props.parse_lines("\ftask_statistics = ", lines)
-    val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
-    Log_Info(name, stats, tasks, timing)
+    val stats = if (full_stats) parse_lines("\fML_statistics = ") else Nil
+    val tasks = if (full_stats) parse_lines("\ftask_statistics = ") else Nil
+    val command_timings = parse_lines("\fcommand_timing = ")
+    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
+    Log_Info(name, stats, tasks, command_timings, session_timing)
   }
 
 
@@ -612,16 +651,20 @@
     verbose: Boolean = false,
     sessions: List[String] = Nil): Int =
   {
+    /* session tree and dependencies */
+
     val full_tree = find_sessions(options, more_dirs)
     val (selected, selected_tree) =
       full_tree.selection(requirements, all_sessions, session_groups, sessions)
 
     val deps = dependencies(progress, true, verbose, list_files, selected_tree)
-    val queue = Queue(selected_tree)
 
     def make_stamp(name: String): String =
       sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
 
+
+    /* persistent information */
+
     val (input_dirs, output_dir, browser_info) =
       if (system_mode) {
         val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
@@ -633,6 +676,40 @@
          Path.explode("$ISABELLE_BROWSER_INFO"))
       }
 
+    def find_log(name: String): Option[(Path, Path)] =
+      input_dirs.find(dir => (dir + log(name)).is_file).map(dir => (dir, dir + log(name)))
+
+
+    /* queue with scheduling information */
+
+    def load_timings(name: String): (List[Properties.T], Double) =
+    {
+      val (path, text) =
+        find_log(name + ".gz") match {
+          case Some((_, path)) => (path, File.read_gzip(path))
+          case None =>
+            find_log(name) match {
+              case Some((_, path)) => (path, File.read(path))
+              case None => (Path.current, "")
+            }
+        }
+      try {
+        val info = parse_log(false, text)
+        val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
+        (info.command_timings, session_timing)
+      }
+      catch {
+        case ERROR(msg) =>
+          java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
+        (Nil, 0.0)
+      }
+    }
+
+    val queue = Queue(selected_tree, load_timings)
+
+
+    /* main build process */
+
     // prepare log dir
     Isabelle_System.mkdirs(output_dir + LOG)
 
@@ -718,9 +795,9 @@
 
                 val (current, heap) =
                 {
-                  input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
-                    case Some(dir) =>
-                      read_stamps(dir + log_gz(name)) match {
+                  find_log(name + ".gz") match {
+                    case Some((dir, path)) =>
+                      read_stamps(path) match {
                         case Some((s, h1, h2)) =>
                           val heap = heap_stamp(Some(dir + Path.basic(name)))
                           (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
@@ -740,7 +817,9 @@
                 }
                 else if (parent_result.rc == 0) {
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
-                  val job = new Job(progress, name, info, output, do_output, verbose, browser_info)
+                  val job =
+                    new Job(progress, name, info, output, do_output, verbose, browser_info,
+                      queue.command_timings(name))
                   loop(pending, running + (name -> (parent_result.heap, job)), results)
                 }
                 else {
@@ -754,6 +833,9 @@
         }
     }
 
+
+    /* build results */
+
     val results =
       if (deps.is_empty) {
         progress.echo("### Nothing to build")
diff -r 9ee38fc0bc81 -r 67882f99274e src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/Pure/goal.ML	Thu Feb 21 15:10:04 2013 +0100
@@ -24,8 +24,8 @@
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
-  val fork_name: string -> (unit -> 'a) -> 'a future
-  val fork: (unit -> 'a) -> 'a future
+  val fork_name: string -> int -> (unit -> 'a) -> 'a future
+  val fork: int -> (unit -> 'a) -> 'a future
   val peek_futures: serial -> unit future list
   val reset_futures: unit -> Future.group list
   val future_enabled_level: int -> bool
@@ -134,7 +134,7 @@
 
 in
 
-fun fork_name name e =
+fun fork_name name pri e =
   uninterruptible (fn _ => fn () =>
     let
       val pos = Position.thread_data ();
@@ -143,7 +143,7 @@
 
       val future =
         (singleton o Future.forks)
-          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
+          {name = name, group = NONE, deps = [], pri = pri, interrupts = false}
           (fn () =>
             let
               val task = the (Future.worker_task ());
@@ -167,7 +167,7 @@
       val _ = register_forked id future;
     in future end) ();
 
-fun fork e = fork_name "Goal.fork" e;
+fun fork pri e = fork_name "Goal.fork" pri e;
 
 fun forked_count () = #1 (Synchronized.value forked_proofs);
 
@@ -285,7 +285,7 @@
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
       then result ()
-      else future_result ctxt' (fork result) (Thm.term_of stmt);
+      else future_result ctxt' (fork ~1 result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)