# HG changeset patch
# User wenzelm
# Date 1488209392 -3600
# Node ID 3e9f382fb67e1c9ea8485e64836b3b76ab3dfea8
# Parent  002b4c8c366ebbb75db83b7890560c7a77c263b3
absent timing information means zero, according to 0070053570c4, f235646b1b73;

diff -r 002b4c8c366e -r 3e9f382fb67e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Feb 27 00:00:28 2017 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Feb 27 16:29:52 2017 +0100
@@ -75,8 +75,8 @@
   val exec_id: Document_ID.exec -> transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val add_hook: (transition -> state -> state -> unit) -> unit
-  val get_timing: transition -> Time.time option
-  val put_timing: Time.time option -> transition -> transition
+  val get_timing: transition -> Time.time
+  val put_timing: Time.time -> transition -> transition
   val transition: bool -> transition -> state -> state * (exn * string) option
   val command_errors: bool -> transition -> state -> Runtime.error list * state option
   val command_exception: bool -> transition -> state -> state
@@ -286,7 +286,7 @@
 datatype transition = Transition of
  {name: string,              (*command name*)
   pos: Position.T,           (*source position*)
-  timing: Time.time option,  (*prescient timing information*)
+  timing: Time.time,         (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
 fun make_transition (name, pos, timing, trans) =
@@ -295,7 +295,7 @@
 fun map_transition f (Transition {name, pos, timing, trans}) =
   make_transition (f (name, pos, timing, trans));
 
-val empty = make_transition ("", Position.none, NONE, []);
+val empty = make_transition ("", Position.none, Time.zeroTime, []);
 
 
 (* diagnostics *)
@@ -649,18 +649,11 @@
 val put_result = Proof.map_context o Result.put;
 
 fun timing_estimate include_head elem =
-  let
-    val trs = Thy_Syntax.flat_element elem |> not include_head ? tl;
-    val timings = map get_timing trs;
-  in
-    if forall is_some timings then
-      SOME (fold (curry (op +) o the) timings Time.zeroTime)
-    else NONE
-  end;
+  let val trs = Thy_Syntax.flat_element elem |> not include_head ? tl
+  in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
 
-fun priority NONE = ~1
-  | priority (SOME estimate) =
-      Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
+fun priority estimate =
+  Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
 
 fun proof_future_enabled estimate st =
   (case try proof_of st of
@@ -669,10 +662,7 @@
       not (Proof.is_relevant state) andalso
        (if can (Proof.assert_bottom true) state
         then Goal.future_enabled 1
-        else
-          (case estimate of
-            NONE => Goal.future_enabled 2
-          | SOME t => Goal.future_enabled_timing t)));
+        else Goal.future_enabled 2 orelse Goal.future_enabled_timing estimate));
 
 fun atom_result keywords tr st =
   let
diff -r 002b4c8c366e -r 3e9f382fb67e src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Feb 27 00:00:28 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Mon Feb 27 16:29:52 2017 +0100
@@ -17,7 +17,7 @@
   val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   val loaded_files_current: theory -> bool
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
-  val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time option) -> int ->
+  val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time) -> int ->
     Path.T -> Thy_Header.header -> Position.T -> string -> theory list ->
     theory * (unit -> unit) * int
 end;
diff -r 002b4c8c366e -r 3e9f382fb67e src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Feb 27 00:00:28 2017 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Feb 27 16:29:52 2017 +0100
@@ -16,7 +16,7 @@
   val use_theories:
     {document: bool,
      symbols: HTML.symbols,
-     last_timing: Toplevel.transition -> Time.time option,
+     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
@@ -350,7 +350,8 @@
 
 val use_thys =
   use_theories
-    {document = false, symbols = HTML.no_symbols, last_timing = K NONE, master_dir = Path.current};
+    {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
+      master_dir = Path.current};
 
 val use_thy = use_thys o single;
 
diff -r 002b4c8c366e -r 3e9f382fb67e src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Mon Feb 27 00:00:28 2017 +0100
+++ b/src/Pure/Tools/build.ML	Mon Feb 27 16:29:52 2017 +0100
@@ -31,7 +31,7 @@
       if name = "" then NONE else SOME {file = file, offset = offset, name = name}
   | _ => NONE);
 
-fun lookup_timings timings tr =
+fun get_timings timings tr =
   (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
     SOME {file, offset, name} =>
       (case Symtab.lookup timings file of
@@ -40,7 +40,8 @@
             SOME (name', time) => if name = name' then SOME time else NONE
           | NONE => NONE)
       | NONE => NONE)
-  | NONE => NONE);
+  | NONE => NONE)
+  |> the_default Time.zeroTime;
 
 
 (* session timing *)
@@ -161,7 +162,7 @@
         parent_name (chapter, name)
         verbose;
 
-    val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
+    val last_timing = get_timings (fold update_timings command_timings empty_timings);
 
     val res1 =
       theories |>
@@ -191,8 +192,10 @@
             let open XML.Decode
             in list (pair Options.decode (list (string #> rpair Position.none))) end;
         val res1 =
-          Exn.capture (fn () =>
-            theories |> List.app (build_theories symbols (K NONE) (Path.explode master_dir))) ();
+          Exn.capture
+            (fn () =>
+              theories
+              |> List.app (build_theories symbols (K Time.zeroTime) (Path.explode master_dir))) ();
         val res2 = Exn.capture Session.shutdown ();
         val result =
           (Par_Exn.release_all [res1, res2]; "") handle exn =>