# HG changeset patch
# User wenzelm
# Date 1361292926 -3600
# Node ID 8c3e5fb411398f8da3d083d8bd690093a8eabff4
# Parent  e8ac22bb2b28da803b29e020d7dfc16cbe4b0edf
improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);

diff -r e8ac22bb2b28 -r 8c3e5fb41139 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Feb 19 17:02:52 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Feb 19 17:55:26 2013 +0100
@@ -1188,7 +1188,7 @@
     andalso not (is_relevant state)
   then
     snd (proof2 (fn state' =>
-      Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state)
+      Goal.fork_name "Proof.future_terminal_proof" ~1 (fn () => ((), proof1 meths state'))) state)
   else proof1 meths state;
 
 in
diff -r e8ac22bb2b28 -r 8c3e5fb41139 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Feb 19 17:02:52 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Feb 19 17:55:26 2013 +0100
@@ -703,9 +703,14 @@
         val (body_trs, end_tr) = split_last proof_trs;
         val finish = Context.Theory o Proof_Context.theory_of;
 
+        val timing_estimate = fold (Timing.add o get_timing) proof_trs Timing.zero;
+        val timing_order =
+          Real.floor (Real.max (Math.log10 (Time.toReal (#elapsed timing_estimate)), ~3.0));
+        val pri = Int.min (timing_order - 3, ~1);
+
         val future_proof = Proof.global_future_proof
           (fn prf =>
-            Goal.fork_name "Toplevel.future_proof"
+            Goal.fork_name "Toplevel.future_proof" pri
               (fn () =>
                 let val (result, result_state) =
                   (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
diff -r e8ac22bb2b28 -r 8c3e5fb41139 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Feb 19 17:02:52 2013 +0100
+++ b/src/Pure/goal.ML	Tue Feb 19 17:55:26 2013 +0100
@@ -24,8 +24,8 @@
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
-  val fork_name: string -> (unit -> 'a) -> 'a future
-  val fork: (unit -> 'a) -> 'a future
+  val fork_name: string -> int -> (unit -> 'a) -> 'a future
+  val fork: int -> (unit -> 'a) -> 'a future
   val peek_futures: serial -> unit future list
   val reset_futures: unit -> Future.group list
   val future_enabled_level: int -> bool
@@ -134,7 +134,7 @@
 
 in
 
-fun fork_name name e =
+fun fork_name name pri e =
   uninterruptible (fn _ => fn () =>
     let
       val pos = Position.thread_data ();
@@ -143,7 +143,7 @@
 
       val future =
         (singleton o Future.forks)
-          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
+          {name = name, group = NONE, deps = [], pri = pri, interrupts = false}
           (fn () =>
             let
               val task = the (Future.worker_task ());
@@ -167,7 +167,7 @@
       val _ = register_forked id future;
     in future end) ();
 
-fun fork e = fork_name "Goal.fork" e;
+fun fork pri e = fork_name "Goal.fork" pri e;
 
 fun forked_count () = #1 (Synchronized.value forked_proofs);
 
@@ -285,7 +285,7 @@
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
       then result ()
-      else future_result ctxt' (fork result) (Thm.term_of stmt);
+      else future_result ctxt' (fork ~1 result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)