keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
authorwenzelm
Thu Jun 22 21:44:15 2017 +0200 (24 months ago ago)
changeset 661708cfa8c7ee1f6
parent 66169 fcd09fc36d7f
child 66171 cad55bc7e37d
keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jun 22 21:10:13 2017 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jun 22 21:44:15 2017 +0200
     1.3 @@ -648,14 +648,10 @@
     1.4  val get_result = Result.get o Proof.context_of;
     1.5  val put_result = Proof.map_context o Result.put;
     1.6  
     1.7 -fun timing_estimate include_head elem =
     1.8 -  let val trs = Thy_Syntax.flat_element elem |> not include_head ? tl
     1.9 +fun timing_estimate elem =
    1.10 +  let val trs = tl (Thy_Syntax.flat_element elem)
    1.11    in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
    1.12  
    1.13 -fun priority estimate =
    1.14 -  if estimate = Time.zeroTime then ~1
    1.15 -  else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
    1.16 -
    1.17  fun proof_future_enabled estimate st =
    1.18    (case try proof_of st of
    1.19      NONE => false
    1.20 @@ -670,8 +666,7 @@
    1.21      val st' =
    1.22        if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
    1.23          (Execution.fork
    1.24 -          {name = "Toplevel.diag", pos = pos_of tr,
    1.25 -            pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
    1.26 +          {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
    1.27            (fn () => command tr st); st)
    1.28        else command tr st;
    1.29    in (Result (tr, st'), st') end;
    1.30 @@ -683,7 +678,7 @@
    1.31        let
    1.32          val (head_result, st') = atom_result keywords head_tr st;
    1.33          val (body_elems, end_tr) = element_rest;
    1.34 -        val estimate = timing_estimate false elem;
    1.35 +        val estimate = timing_estimate elem;
    1.36        in
    1.37          if not (proof_future_enabled estimate st')
    1.38          then
    1.39 @@ -698,7 +693,7 @@
    1.40              val future_proof =
    1.41                Proof.future_proof (fn state =>
    1.42                  Execution.fork
    1.43 -                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate}
    1.44 +                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
    1.45                    (fn () =>
    1.46                      let
    1.47                        val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';