absent timing information means zero, according to 0070053570c4, f235646b1b73;
authorwenzelm
Mon Feb 27 16:29:52 2017 +0100 (2017-02-27 ago)
changeset 650583e9f382fb67e
parent 65056 002b4c8c366e
child 65059 05f1b5342298
absent timing information means zero, according to 0070053570c4, f235646b1b73;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/resources.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Feb 27 00:00:28 2017 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Feb 27 16:29:52 2017 +0100
     1.3 @@ -75,8 +75,8 @@
     1.4    val exec_id: Document_ID.exec -> transition -> transition
     1.5    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
     1.6    val add_hook: (transition -> state -> state -> unit) -> unit
     1.7 -  val get_timing: transition -> Time.time option
     1.8 -  val put_timing: Time.time option -> transition -> transition
     1.9 +  val get_timing: transition -> Time.time
    1.10 +  val put_timing: Time.time -> transition -> transition
    1.11    val transition: bool -> transition -> state -> state * (exn * string) option
    1.12    val command_errors: bool -> transition -> state -> Runtime.error list * state option
    1.13    val command_exception: bool -> transition -> state -> state
    1.14 @@ -286,7 +286,7 @@
    1.15  datatype transition = Transition of
    1.16   {name: string,              (*command name*)
    1.17    pos: Position.T,           (*source position*)
    1.18 -  timing: Time.time option,  (*prescient timing information*)
    1.19 +  timing: Time.time,         (*prescient timing information*)
    1.20    trans: trans list};        (*primitive transitions (union)*)
    1.21  
    1.22  fun make_transition (name, pos, timing, trans) =
    1.23 @@ -295,7 +295,7 @@
    1.24  fun map_transition f (Transition {name, pos, timing, trans}) =
    1.25    make_transition (f (name, pos, timing, trans));
    1.26  
    1.27 -val empty = make_transition ("", Position.none, NONE, []);
    1.28 +val empty = make_transition ("", Position.none, Time.zeroTime, []);
    1.29  
    1.30  
    1.31  (* diagnostics *)
    1.32 @@ -649,18 +649,11 @@
    1.33  val put_result = Proof.map_context o Result.put;
    1.34  
    1.35  fun timing_estimate include_head elem =
    1.36 -  let
    1.37 -    val trs = Thy_Syntax.flat_element elem |> not include_head ? tl;
    1.38 -    val timings = map get_timing trs;
    1.39 -  in
    1.40 -    if forall is_some timings then
    1.41 -      SOME (fold (curry (op +) o the) timings Time.zeroTime)
    1.42 -    else NONE
    1.43 -  end;
    1.44 +  let val trs = Thy_Syntax.flat_element elem |> not include_head ? tl
    1.45 +  in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
    1.46  
    1.47 -fun priority NONE = ~1
    1.48 -  | priority (SOME estimate) =
    1.49 -      Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
    1.50 +fun priority estimate =
    1.51 +  Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
    1.52  
    1.53  fun proof_future_enabled estimate st =
    1.54    (case try proof_of st of
    1.55 @@ -669,10 +662,7 @@
    1.56        not (Proof.is_relevant state) andalso
    1.57         (if can (Proof.assert_bottom true) state
    1.58          then Goal.future_enabled 1
    1.59 -        else
    1.60 -          (case estimate of
    1.61 -            NONE => Goal.future_enabled 2
    1.62 -          | SOME t => Goal.future_enabled_timing t)));
    1.63 +        else Goal.future_enabled 2 orelse Goal.future_enabled_timing estimate));
    1.64  
    1.65  fun atom_result keywords tr st =
    1.66    let
     2.1 --- a/src/Pure/PIDE/resources.ML	Mon Feb 27 00:00:28 2017 +0100
     2.2 +++ b/src/Pure/PIDE/resources.ML	Mon Feb 27 16:29:52 2017 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
     2.5    val loaded_files_current: theory -> bool
     2.6    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     2.7 -  val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time option) -> int ->
     2.8 +  val load_thy: bool -> HTML.symbols -> (Toplevel.transition -> Time.time) -> int ->
     2.9      Path.T -> Thy_Header.header -> Position.T -> string -> theory list ->
    2.10      theory * (unit -> unit) * int
    2.11  end;
     3.1 --- a/src/Pure/Thy/thy_info.ML	Mon Feb 27 00:00:28 2017 +0100
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Feb 27 16:29:52 2017 +0100
     3.3 @@ -16,7 +16,7 @@
     3.4    val use_theories:
     3.5      {document: bool,
     3.6       symbols: HTML.symbols,
     3.7 -     last_timing: Toplevel.transition -> Time.time option,
     3.8 +     last_timing: Toplevel.transition -> Time.time,
     3.9       master_dir: Path.T} -> (string * Position.T) list -> unit
    3.10    val use_thys: (string * Position.T) list -> unit
    3.11    val use_thy: string * Position.T -> unit
    3.12 @@ -350,7 +350,8 @@
    3.13  
    3.14  val use_thys =
    3.15    use_theories
    3.16 -    {document = false, symbols = HTML.no_symbols, last_timing = K NONE, master_dir = Path.current};
    3.17 +    {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
    3.18 +      master_dir = Path.current};
    3.19  
    3.20  val use_thy = use_thys o single;
    3.21  
     4.1 --- a/src/Pure/Tools/build.ML	Mon Feb 27 00:00:28 2017 +0100
     4.2 +++ b/src/Pure/Tools/build.ML	Mon Feb 27 16:29:52 2017 +0100
     4.3 @@ -31,7 +31,7 @@
     4.4        if name = "" then NONE else SOME {file = file, offset = offset, name = name}
     4.5    | _ => NONE);
     4.6  
     4.7 -fun lookup_timings timings tr =
     4.8 +fun get_timings timings tr =
     4.9    (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
    4.10      SOME {file, offset, name} =>
    4.11        (case Symtab.lookup timings file of
    4.12 @@ -40,7 +40,8 @@
    4.13              SOME (name', time) => if name = name' then SOME time else NONE
    4.14            | NONE => NONE)
    4.15        | NONE => NONE)
    4.16 -  | NONE => NONE);
    4.17 +  | NONE => NONE)
    4.18 +  |> the_default Time.zeroTime;
    4.19  
    4.20  
    4.21  (* session timing *)
    4.22 @@ -161,7 +162,7 @@
    4.23          parent_name (chapter, name)
    4.24          verbose;
    4.25  
    4.26 -    val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
    4.27 +    val last_timing = get_timings (fold update_timings command_timings empty_timings);
    4.28  
    4.29      val res1 =
    4.30        theories |>
    4.31 @@ -191,8 +192,10 @@
    4.32              let open XML.Decode
    4.33              in list (pair Options.decode (list (string #> rpair Position.none))) end;
    4.34          val res1 =
    4.35 -          Exn.capture (fn () =>
    4.36 -            theories |> List.app (build_theories symbols (K NONE) (Path.explode master_dir))) ();
    4.37 +          Exn.capture
    4.38 +            (fn () =>
    4.39 +              theories
    4.40 +              |> List.app (build_theories symbols (K Time.zeroTime) (Path.explode master_dir))) ();
    4.41          val res2 = Exn.capture Session.shutdown ();
    4.42          val result =
    4.43            (Par_Exn.release_all [res1, res2]; "") handle exn =>