1.1 --- a/src/Pure/Isar/proof.ML	Tue Feb 19 17:02:52 2013 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Feb 19 17:55:26 2013 +0100
     1.3 @@ -1188,7 +1188,7 @@
     1.4      andalso not (is_relevant state)
     1.5    then
     1.6      snd (proof2 (fn state' =>
     1.7 -      Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state)
     1.8 +      Goal.fork_name "Proof.future_terminal_proof" ~1 (fn () => ((), proof1 meths state'))) state)
     1.9    else proof1 meths state;
    1.10  
    1.11  in

     2.1 --- a/src/Pure/Isar/toplevel.ML	Tue Feb 19 17:02:52 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Feb 19 17:55:26 2013 +0100
     2.3 @@ -703,9 +703,14 @@
     2.4          val (body_trs, end_tr) = split_last proof_trs;
     2.5          val finish = Context.Theory o Proof_Context.theory_of;
     2.6  
     2.7 +        val timing_estimate = fold (Timing.add o get_timing) proof_trs Timing.zero;
     2.8 +        val timing_order =
     2.9 +          Real.floor (Real.max (Math.log10 (Time.toReal (#elapsed timing_estimate)), ~3.0));
    2.10 +        val pri = Int.min (timing_order - 3, ~1);
    2.11 +
    2.12          val future_proof = Proof.global_future_proof
    2.13            (fn prf =>
    2.14 -            Goal.fork_name "Toplevel.future_proof"
    2.15 +            Goal.fork_name "Toplevel.future_proof" pri
    2.16                (fn () =>
    2.17                  let val (result, result_state) =
    2.18                    (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)

     3.1 --- a/src/Pure/goal.ML	Tue Feb 19 17:02:52 2013 +0100
     3.2 +++ b/src/Pure/goal.ML	Tue Feb 19 17:55:26 2013 +0100
     3.3 @@ -24,8 +24,8 @@
     3.4    val check_finished: Proof.context -> thm -> thm
     3.5    val finish: Proof.context -> thm -> thm
     3.6    val norm_result: thm -> thm
     3.7 -  val fork_name: string -> (unit -> 'a) -> 'a future
     3.8 -  val fork: (unit -> 'a) -> 'a future
     3.9 +  val fork_name: string -> int -> (unit -> 'a) -> 'a future
    3.10 +  val fork: int -> (unit -> 'a) -> 'a future
    3.11    val peek_futures: serial -> unit future list
    3.12    val reset_futures: unit -> Future.group list
    3.13    val future_enabled_level: int -> bool
    3.14 @@ -134,7 +134,7 @@
    3.15  
    3.16  in
    3.17  
    3.18 -fun fork_name name e =
    3.19 +fun fork_name name pri e =
    3.20    uninterruptible (fn _ => fn () =>
    3.21      let
    3.22        val pos = Position.thread_data ();
    3.23 @@ -143,7 +143,7 @@
    3.24  
    3.25        val future =
    3.26          (singleton o Future.forks)
    3.27 -          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
    3.28 +          {name = name, group = NONE, deps = [], pri = pri, interrupts = false}
    3.29            (fn () =>
    3.30              let
    3.31                val task = the (Future.worker_task ());
    3.32 @@ -167,7 +167,7 @@
    3.33        val _ = register_forked id future;
    3.34      in future end) ();
    3.35  
    3.36 -fun fork e = fork_name "Goal.fork" e;
    3.37 +fun fork pri e = fork_name "Goal.fork" pri e;
    3.38  
    3.39  fun forked_count () = #1 (Synchronized.value forked_proofs);
    3.40  
    3.41 @@ -285,7 +285,7 @@
    3.42      val res =
    3.43        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
    3.44        then result ()
    3.45 -      else future_result ctxt' (fork result) (Thm.term_of stmt);
    3.46 +      else future_result ctxt' (fork ~1 result) (Thm.term_of stmt);
    3.47    in
    3.48      Conjunction.elim_balanced (length props) res
    3.49      |> map (Assumption.export false ctxt' ctxt)