1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Mar 01 22:15:31 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Mar 03 13:23:06 2013 +0100
     1.3 @@ -710,8 +710,10 @@
     1.4    fun init _ = empty;
     1.5  );
     1.6  
     1.7 -fun priority trs =
     1.8 -  let val estimate = fold (curry Time.+ o get_timing) trs Time.zeroTime in
     1.9 +fun priority elem =
    1.10 +  let
    1.11 +    val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem Time.zeroTime;
    1.12 +  in
    1.13      if estimate = Time.zeroTime then ~1
    1.14      else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
    1.15    end;
    1.16 @@ -725,7 +727,8 @@
    1.17          val st' =
    1.18            if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
    1.19              setmp_thread_position tr (fn () =>
    1.20 -              (Goal.fork_name "Toplevel.diag" (priority [tr]) (fn () => command tr st); st)) ()
    1.21 +              (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
    1.22 +                (fn () => command tr st); st)) ()
    1.23            else command tr st;
    1.24        in ((tr, st'), st') end;
    1.25  
    1.26 @@ -749,7 +752,8 @@
    1.27          val future_proof = Proof.future_proof
    1.28            (fn prf =>
    1.29              setmp_thread_position head_tr (fn () =>
    1.30 -              Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
    1.31 +              Goal.fork_name "Toplevel.future_proof"
    1.32 +                (priority (Thy_Syntax.Element (empty, opt_proof)))
    1.33                  (fn () =>
    1.34                    let val (result, result_state) =
    1.35                      (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)

     2.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Mar 01 22:15:31 2013 +0100
     2.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sun Mar 03 13:23:06 2013 +0100
     2.3 @@ -16,6 +16,8 @@
     2.4    val present_span: span -> Output.output
     2.5    val parse_spans: Token.T list -> span list
     2.6    datatype 'a element = Element of 'a * ('a element list * 'a) option
     2.7 +  val atom: 'a -> 'a element
     2.8 +  val fold_element: ('a -> 'b -> 'b) -> 'a element -> 'b -> 'b
     2.9    val map_element: ('a -> 'b) -> 'a element -> 'b element
    2.10    val flat_element: 'a element -> 'a list
    2.11    val last_element: 'a element -> 'a
    2.12 @@ -142,6 +144,9 @@
    2.13  fun element (a, b) = Element (a, SOME b);
    2.14  fun atom a = Element (a, NONE);
    2.15  
    2.16 +fun fold_element f (Element (a, NONE)) = f a
    2.17 +  | fold_element f (Element (a, SOME (elems, b))) = f a #> (fold o fold_element) f elems #> f b;
    2.18 +
    2.19  fun map_element f (Element (a, NONE)) = Element (f a, NONE)
    2.20    | map_element f (Element (a, SOME (elems, b))) =
    2.21        Element (f a, SOME ((map o map_element) f elems, f b));