more explicit Goal.fork_params -- avoid implicit arguments via thread data;
actually fork terminal proofs in interactive mode (amending 8707df0b0255);
--- 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;
--- 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 =
--- 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 =
--- 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);