more explicit Goal.fork_params -- avoid implicit arguments via thread data;
authorwenzelm
Wed Apr 03 21:30:32 2013 +0200 (2013-04-03 ago)
changeset 51605eca8acb42e4a
parent 51604 f83661733143
child 51606 2843cc095a57
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
actually fork terminal proofs in interactive mode (amending 8707df0b0255);
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Apr 03 20:56:08 2013 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Apr 03 21:30:32 2013 +0200
     1.3 @@ -1158,24 +1158,23 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun future_terminal_proof n proof1 proof2 done int state =
     1.8 -  if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int)
     1.9 -    andalso not (is_relevant state)
    1.10 -  then
    1.11 +fun future_terminal_proof proof1 proof2 done int state =
    1.12 +  if Goal.future_enabled_level 3 andalso not (is_relevant state) then
    1.13      state |> future_proof (fn state' =>
    1.14 -      Goal.fork_name "Proof.future_terminal_proof" ~1
    1.15 +      Goal.fork_params
    1.16 +        {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
    1.17          (fn () => ((), proof2 state'))) |> snd |> done
    1.18    else proof1 state;
    1.19  
    1.20  in
    1.21  
    1.22  fun local_future_terminal_proof meths =
    1.23 -  future_terminal_proof 3
    1.24 +  future_terminal_proof
    1.25      (local_terminal_proof meths)
    1.26      (local_terminal_proof meths #> context_of) local_done_proof;
    1.27  
    1.28  fun global_future_terminal_proof meths =
    1.29 -  future_terminal_proof 3
    1.30 +  future_terminal_proof
    1.31      (global_terminal_proof meths)
    1.32      (global_terminal_proof meths) global_done_proof;
    1.33  
     2.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 03 20:56:08 2013 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 03 21:30:32 2013 +0200
     2.3 @@ -763,9 +763,10 @@
     2.4    let
     2.5      val st' =
     2.6        if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
     2.7 -        setmp_thread_position tr (fn () =>
     2.8 -          (Goal.fork_name "Toplevel.diag" (priority (timing_estimate true (Thy_Syntax.atom tr)))
     2.9 -            (fn () => command tr st); st)) ()
    2.10 +        (Goal.fork_params
    2.11 +          {name = "Toplevel.diag", pos = pos_of tr,
    2.12 +            pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
    2.13 +          (fn () => command tr st); st)
    2.14        else command tr st;
    2.15    in (Result (tr, st'), st') end;
    2.16  
    2.17 @@ -788,19 +789,18 @@
    2.18            let
    2.19              val finish = Context.Theory o Proof_Context.theory_of;
    2.20  
    2.21 -            val future_proof = Proof.future_proof
    2.22 -              (fn state =>
    2.23 -                setmp_thread_position head_tr (fn () =>
    2.24 -                  Goal.fork_name "Toplevel.future_proof"
    2.25 -                    (priority estimate)
    2.26 -                    (fn () =>
    2.27 -                      let
    2.28 -                        val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
    2.29 -                        val prf' = Proof_Node.apply (K state) prf;
    2.30 -                        val (result, result_state) =
    2.31 -                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
    2.32 -                          |> fold_map element_result body_elems ||> command end_tr;
    2.33 -                      in (Result_List result, presentation_context_of result_state) end)) ())
    2.34 +            val future_proof =
    2.35 +              Proof.future_proof (fn state =>
    2.36 +                Goal.fork_params
    2.37 +                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate}
    2.38 +                  (fn () =>
    2.39 +                    let
    2.40 +                      val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
    2.41 +                      val prf' = Proof_Node.apply (K state) prf;
    2.42 +                      val (result, result_state) =
    2.43 +                        State (SOME (Proof (prf', (finish, orig_gthy))), prev)
    2.44 +                        |> fold_map element_result body_elems ||> command end_tr;
    2.45 +                    in (Result_List result, presentation_context_of result_state) end))
    2.46                #> (fn (res, state') => state' |> put_result (Result_Future res));
    2.47  
    2.48              val forked_proof =
     3.1 --- a/src/Pure/PIDE/command.ML	Wed Apr 03 20:56:08 2013 +0200
     3.2 +++ b/src/Pure/PIDE/command.ML	Wed Apr 03 21:30:32 2013 +0200
     3.3 @@ -63,9 +63,8 @@
     3.4  
     3.5  fun run int tr st =
     3.6    if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
     3.7 -    Toplevel.setmp_thread_position tr (fn () =>
     3.8 -      (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st);
     3.9 -        ([], SOME st))) ()
    3.10 +    (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
    3.11 +      (fn () => Toplevel.command_exception int tr st); ([], SOME st))
    3.12    else Toplevel.command_errors int tr st;
    3.13  
    3.14  fun check_cmts tr cmts st =
     4.1 --- a/src/Pure/goal.ML	Wed Apr 03 20:56:08 2013 +0200
     4.2 +++ b/src/Pure/goal.ML	Wed Apr 03 21:30:32 2013 +0200
     4.3 @@ -26,7 +26,7 @@
     4.4    val check_finished: Proof.context -> thm -> thm
     4.5    val finish: Proof.context -> thm -> thm
     4.6    val norm_result: thm -> thm
     4.7 -  val fork_name: string -> int -> (unit -> 'a) -> 'a future
     4.8 +  val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
     4.9    val fork: int -> (unit -> 'a) -> 'a future
    4.10    val peek_futures: serial -> unit future list
    4.11    val reset_futures: unit -> Future.group list
    4.12 @@ -143,10 +143,9 @@
    4.13  
    4.14  in
    4.15  
    4.16 -fun fork_name name pri e =
    4.17 +fun fork_params {name, pos, pri} e =
    4.18    uninterruptible (fn _ => fn () =>
    4.19      let
    4.20 -      val pos = Position.thread_data ();
    4.21        val id = the_default 0 (Position.parse_id pos);
    4.22        val _ = count_forked 1;
    4.23  
    4.24 @@ -176,7 +175,8 @@
    4.25        val _ = register_forked id future;
    4.26      in future end) ();
    4.27  
    4.28 -fun fork pri e = fork_name "Goal.fork" pri e;
    4.29 +fun fork pri e =
    4.30 +  fork_params {name = "Goal.fork", pos = Position.thread_data (), pri = pri} e;
    4.31  
    4.32  fun forked_count () = #1 (Synchronized.value forked_proofs);
    4.33