clarified priority: zero can mean unknown/long or irrelevant/short time;
authorwenzelm
Mon Feb 27 17:50:29 2017 +0100 (2017-02-27 ago)
changeset 6505905f1b5342298
parent 65058 3e9f382fb67e
child 65060 98931050065f
clarified priority: zero can mean unknown/long or irrelevant/short time;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Feb 27 16:29:52 2017 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Feb 27 17:50:29 2017 +0100
     1.3 @@ -653,7 +653,8 @@
     1.4    in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
     1.5  
     1.6  fun priority estimate =
     1.7 -  Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
     1.8 +  if estimate = Time.zeroTime then ~1
     1.9 +  else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
    1.10  
    1.11  fun proof_future_enabled estimate st =
    1.12    (case try proof_of st of