# HG changeset patch
# User wenzelm
# Date 1365017432 -7200
# Node ID eca8acb42e4a74808403312a85a483e3274631d3
# Parent  f836617331431dbca95926176e01e1bc5b72c13b
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
actually fork terminal proofs in interactive mode (amending 8707df0b0255);

diff -r f83661733143 -r eca8acb42e4a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Apr 03 20:56:08 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 03 21:30:32 2013 +0200
@@ -1158,24 +1158,23 @@
 
 local
 
-fun future_terminal_proof n proof1 proof2 done int state =
-  if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int)
-    andalso not (is_relevant state)
-  then
+fun future_terminal_proof proof1 proof2 done int state =
+  if Goal.future_enabled_level 3 andalso not (is_relevant state) then
     state |> future_proof (fn state' =>
-      Goal.fork_name "Proof.future_terminal_proof" ~1
+      Goal.fork_params
+        {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
         (fn () => ((), proof2 state'))) |> snd |> done
   else proof1 state;
 
 in
 
 fun local_future_terminal_proof meths =
-  future_terminal_proof 3
+  future_terminal_proof
     (local_terminal_proof meths)
     (local_terminal_proof meths #> context_of) local_done_proof;
 
 fun global_future_terminal_proof meths =
-  future_terminal_proof 3
+  future_terminal_proof
     (global_terminal_proof meths)
     (global_terminal_proof meths) global_done_proof;
 
diff -r f83661733143 -r eca8acb42e4a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Apr 03 20:56:08 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Apr 03 21:30:32 2013 +0200
@@ -763,9 +763,10 @@
   let
     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 (timing_estimate true (Thy_Syntax.atom tr)))
-            (fn () => command tr st); st)) ()
+        (Goal.fork_params
+          {name = "Toplevel.diag", pos = pos_of tr,
+            pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
+          (fn () => command tr st); st)
       else command tr st;
   in (Result (tr, st'), st') end;
 
@@ -788,19 +789,18 @@
           let
             val finish = Context.Theory o Proof_Context.theory_of;
 
-            val future_proof = Proof.future_proof
-              (fn state =>
-                setmp_thread_position head_tr (fn () =>
-                  Goal.fork_name "Toplevel.future_proof"
-                    (priority estimate)
-                    (fn () =>
-                      let
-                        val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
-                        val prf' = Proof_Node.apply (K state) prf;
-                        val (result, result_state) =
-                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
-                          |> fold_map element_result body_elems ||> command end_tr;
-                      in (Result_List result, presentation_context_of result_state) end)) ())
+            val future_proof =
+              Proof.future_proof (fn state =>
+                Goal.fork_params
+                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate}
+                  (fn () =>
+                    let
+                      val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
+                      val prf' = Proof_Node.apply (K state) prf;
+                      val (result, result_state) =
+                        State (SOME (Proof (prf', (finish, orig_gthy))), prev)
+                        |> fold_map element_result body_elems ||> command end_tr;
+                    in (Result_List result, presentation_context_of result_state) end))
               #> (fn (res, state') => state' |> put_result (Result_Future res));
 
             val forked_proof =
diff -r f83661733143 -r eca8acb42e4a src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Apr 03 20:56:08 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Apr 03 21:30:32 2013 +0200
@@ -63,9 +63,8 @@
 
 fun run int tr st =
   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
-    Toplevel.setmp_thread_position tr (fn () =>
-      (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st);
-        ([], SOME st))) ()
+    (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
+      (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   else Toplevel.command_errors int tr st;
 
 fun check_cmts tr cmts st =
diff -r f83661733143 -r eca8acb42e4a src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Apr 03 20:56:08 2013 +0200
+++ b/src/Pure/goal.ML	Wed Apr 03 21:30:32 2013 +0200
@@ -26,7 +26,7 @@
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
-  val fork_name: string -> int -> (unit -> 'a) -> 'a future
+  val fork_params: {name: string, pos: Position.T, pri: 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
@@ -143,10 +143,9 @@
 
 in
 
-fun fork_name name pri e =
+fun fork_params {name, pos, pri} e =
   uninterruptible (fn _ => fn () =>
     let
-      val pos = Position.thread_data ();
       val id = the_default 0 (Position.parse_id pos);
       val _ = count_forked 1;
 
@@ -176,7 +175,8 @@
       val _ = register_forked id future;
     in future end) ();
 
-fun fork pri e = fork_name "Goal.fork" pri e;
+fun fork pri e =
+  fork_params {name = "Goal.fork", pos = Position.thread_data (), pri = pri} e;
 
 fun forked_count () = #1 (Synchronized.value forked_proofs);