src/Pure/Isar/toplevel.ML
changeset 51423 e5f9a6d9ca82
parent 51332 8707df0b0255
child 51553 63327f679cff
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 13 17:15:25 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 13 21:25:08 2013 +0100
     1.3 @@ -91,8 +91,8 @@
     1.4    val status: transition -> Markup.T -> unit
     1.5    val add_hook: (transition -> state -> state -> unit) -> unit
     1.6    val approximative_id: transition -> {file: string, offset: int, name: string} option
     1.7 -  val get_timing: transition -> Time.time
     1.8 -  val put_timing: Time.time -> transition -> transition
     1.9 +  val get_timing: transition -> Time.time option
    1.10 +  val put_timing: Time.time option -> transition -> transition
    1.11    val transition: bool -> transition -> state -> (state * (exn * string) option) 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 @@ -346,7 +346,7 @@
    1.15    int_only: bool,            (*interactive-only*)
    1.16    print: bool,               (*print result state*)
    1.17    no_timing: bool,           (*suppress timing*)
    1.18 -  timing: Time.time,         (*prescient timing information*)
    1.19 +  timing: Time.time option,  (*prescient timing information*)
    1.20    trans: trans list};        (*primitive transitions (union)*)
    1.21  
    1.22  fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
    1.23 @@ -356,7 +356,7 @@
    1.24  fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
    1.25    make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
    1.26  
    1.27 -val empty = make_transition ("", Position.none, false, false, false, Time.zeroTime, []);
    1.28 +val empty = make_transition ("", Position.none, false, false, false, NONE, []);
    1.29  
    1.30  
    1.31  (* diagnostics *)
    1.32 @@ -638,14 +638,12 @@
    1.33  local
    1.34  
    1.35  fun timing_message tr (t: Timing.timing) =
    1.36 -  if Timing.is_relevant_time (#elapsed t) then
    1.37 -    (case approximative_id tr of
    1.38 -      SOME id =>
    1.39 -        (Output.protocol_message
    1.40 -          (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
    1.41 -        handle Fail _ => ())
    1.42 -    | NONE => ())
    1.43 -  else ();
    1.44 +  (case approximative_id tr of
    1.45 +    SOME id =>
    1.46 +      (Output.protocol_message
    1.47 +        (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
    1.48 +      handle Fail _ => ())
    1.49 +  | NONE => ());
    1.50  
    1.51  fun app int (tr as Transition {trans, print, no_timing, ...}) =
    1.52    setmp_thread_position tr (fn state =>
    1.53 @@ -727,29 +725,38 @@
    1.54  val get_result = Result.get o Proof.context_of;
    1.55  val put_result = Proof.map_context o Result.put;
    1.56  
    1.57 -fun proof_future_enabled st =
    1.58 +fun timing_estimate include_head elem =
    1.59 +  let
    1.60 +    val trs = Thy_Syntax.flat_element elem |> not include_head ? tl;
    1.61 +    val timings = map get_timing trs;
    1.62 +  in
    1.63 +    if forall is_some timings then
    1.64 +      SOME (fold (curry Time.+ o the) timings Time.zeroTime)
    1.65 +    else NONE
    1.66 +  end;
    1.67 +
    1.68 +fun priority NONE = ~1
    1.69 +  | priority (SOME estimate) =
    1.70 +      Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
    1.71 +
    1.72 +fun proof_future_enabled estimate st =
    1.73    (case try proof_of st of
    1.74      NONE => false
    1.75    | SOME state =>
    1.76        not (Proof.is_relevant state) andalso
    1.77         (if can (Proof.assert_bottom true) state
    1.78          then Goal.future_enabled ()
    1.79 -        else Goal.future_enabled_nested 2));
    1.80 -
    1.81 -fun priority elem =
    1.82 -  let
    1.83 -    val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem Time.zeroTime;
    1.84 -  in
    1.85 -    if estimate = Time.zeroTime then ~1
    1.86 -    else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
    1.87 -  end;
    1.88 +        else
    1.89 +          (case estimate of
    1.90 +            NONE => Goal.future_enabled_nested 2
    1.91 +          | SOME t => Goal.future_enabled_timing t)));
    1.92  
    1.93  fun atom_result tr st =
    1.94    let
    1.95      val st' =
    1.96        if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
    1.97          setmp_thread_position tr (fn () =>
    1.98 -          (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
    1.99 +          (Goal.fork_name "Toplevel.diag" (priority (timing_estimate true (Thy_Syntax.atom tr)))
   1.100              (fn () => command tr st); st)) ()
   1.101        else command tr st;
   1.102    in (Result (tr, st'), st') end;
   1.103 @@ -757,12 +764,13 @@
   1.104  in
   1.105  
   1.106  fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
   1.107 -  | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
   1.108 +  | element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
   1.109        let
   1.110          val (head_result, st') = atom_result head_tr st;
   1.111          val (body_elems, end_tr) = element_rest;
   1.112 +        val estimate = timing_estimate false elem;
   1.113        in
   1.114 -        if not (proof_future_enabled st')
   1.115 +        if not (proof_future_enabled estimate st')
   1.116          then
   1.117            let
   1.118              val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
   1.119 @@ -776,7 +784,7 @@
   1.120                (fn state =>
   1.121                  setmp_thread_position head_tr (fn () =>
   1.122                    Goal.fork_name "Toplevel.future_proof"
   1.123 -                    (priority (Thy_Syntax.Element (empty, SOME element_rest)))
   1.124 +                    (priority estimate)
   1.125                      (fn () =>
   1.126                        let
   1.127                          val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';