# HG changeset patch
# User wenzelm
# Date 1362313386 -3600
# Node ID 75682dfff630e75adfb4aa2a6af7c52eece643c0
# Parent  c1cb872ccb2bbe97f336282da2b116457a44f2d9
more Thy_Syntax.element operations;

diff -r c1cb872ccb2b -r 75682dfff630 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Mar 01 22:15:31 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Mar 03 13:23:06 2013 +0100
@@ -710,8 +710,10 @@
   fun init _ = empty;
 );
 
-fun priority trs =
-  let val estimate = fold (curry Time.+ o get_timing) trs Time.zeroTime in
+fun priority elem =
+  let
+    val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem Time.zeroTime;
+  in
     if estimate = Time.zeroTime then ~1
     else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
   end;
@@ -725,7 +727,8 @@
         val st' =
           if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
             setmp_thread_position tr (fn () =>
-              (Goal.fork_name "Toplevel.diag" (priority [tr]) (fn () => command tr st); st)) ()
+              (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
+                (fn () => command tr st); st)) ()
           else command tr st;
       in ((tr, st'), st') end;
 
@@ -749,7 +752,8 @@
         val future_proof = Proof.future_proof
           (fn prf =>
             setmp_thread_position head_tr (fn () =>
-              Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
+              Goal.fork_name "Toplevel.future_proof"
+                (priority (Thy_Syntax.Element (empty, opt_proof)))
                 (fn () =>
                   let val (result, result_state) =
                     (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
diff -r c1cb872ccb2b -r 75682dfff630 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Fri Mar 01 22:15:31 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Sun Mar 03 13:23:06 2013 +0100
@@ -16,6 +16,8 @@
   val present_span: span -> Output.output
   val parse_spans: Token.T list -> span list
   datatype 'a element = Element of 'a * ('a element list * 'a) option
+  val atom: 'a -> 'a element
+  val fold_element: ('a -> 'b -> 'b) -> 'a element -> 'b -> 'b
   val map_element: ('a -> 'b) -> 'a element -> 'b element
   val flat_element: 'a element -> 'a list
   val last_element: 'a element -> 'a
@@ -142,6 +144,9 @@
 fun element (a, b) = Element (a, SOME b);
 fun atom a = Element (a, NONE);
 
+fun fold_element f (Element (a, NONE)) = f a
+  | fold_element f (Element (a, SOME (elems, b))) = f a #> (fold o fold_element) f elems #> f b;
+
 fun map_element f (Element (a, NONE)) = Element (f a, NONE)
   | map_element f (Element (a, SOME (elems, b))) =
       Element (f a, SOME ((map o map_element) f elems, f b));