src/Pure/Isar/toplevel.ML
changeset 51605 eca8acb42e4a
parent 51595 8e9746e584c9
child 51658 21c10672633b
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 03 20:56:08 2013 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 03 21:30:32 2013 +0200
     1.3 @@ -763,9 +763,10 @@
     1.4    let
     1.5      val st' =
     1.6        if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
     1.7 -        setmp_thread_position tr (fn () =>
     1.8 -          (Goal.fork_name "Toplevel.diag" (priority (timing_estimate true (Thy_Syntax.atom tr)))
     1.9 -            (fn () => command tr st); st)) ()
    1.10 +        (Goal.fork_params
    1.11 +          {name = "Toplevel.diag", pos = pos_of tr,
    1.12 +            pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
    1.13 +          (fn () => command tr st); st)
    1.14        else command tr st;
    1.15    in (Result (tr, st'), st') end;
    1.16  
    1.17 @@ -788,19 +789,18 @@
    1.18            let
    1.19              val finish = Context.Theory o Proof_Context.theory_of;
    1.20  
    1.21 -            val future_proof = Proof.future_proof
    1.22 -              (fn state =>
    1.23 -                setmp_thread_position head_tr (fn () =>
    1.24 -                  Goal.fork_name "Toplevel.future_proof"
    1.25 -                    (priority estimate)
    1.26 -                    (fn () =>
    1.27 -                      let
    1.28 -                        val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
    1.29 -                        val prf' = Proof_Node.apply (K state) prf;
    1.30 -                        val (result, result_state) =
    1.31 -                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
    1.32 -                          |> fold_map element_result body_elems ||> command end_tr;
    1.33 -                      in (Result_List result, presentation_context_of result_state) end)) ())
    1.34 +            val future_proof =
    1.35 +              Proof.future_proof (fn state =>
    1.36 +                Goal.fork_params
    1.37 +                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate}
    1.38 +                  (fn () =>
    1.39 +                    let
    1.40 +                      val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
    1.41 +                      val prf' = Proof_Node.apply (K state) prf;
    1.42 +                      val (result, result_state) =
    1.43 +                        State (SOME (Proof (prf', (finish, orig_gthy))), prev)
    1.44 +                        |> fold_map element_result body_elems ||> command end_tr;
    1.45 +                    in (Result_List result, presentation_context_of result_state) end))
    1.46                #> (fn (res, state') => state' |> put_result (Result_Future res));
    1.47  
    1.48              val forked_proof =