simplified Proof.future_proof;
authorwenzelm
Thu Feb 28 21:11:07 2013 +0100 (2013-02-28 ago)
changeset 51318e6524a89c9e3
parent 51317 0e70cc4e94e8
child 51319 4a92178011e7
simplified Proof.future_proof;
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Feb 28 18:35:31 2013 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Feb 28 21:11:07 2013 +0100
     1.3 @@ -115,8 +115,7 @@
     1.4      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
     1.5    val schematic_goal: state -> bool
     1.6    val is_relevant: state -> bool
     1.7 -  val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
     1.8 -  val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
     1.9 +  val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
    1.10    val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
    1.11      state -> state
    1.12    val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
    1.13 @@ -1140,7 +1139,9 @@
    1.14  val set_result = Result.put o SOME;
    1.15  val reset_result = Result.put NONE;
    1.16  
    1.17 -fun future_proof done get_context fork_proof state =
    1.18 +in
    1.19 +
    1.20 +fun future_proof fork_proof state =
    1.21    let
    1.22      val _ = assert_backward state;
    1.23      val (goal_ctxt, (_, goal)) = find_goal state;
    1.24 @@ -1164,18 +1165,12 @@
    1.25          (fold (Variable.declare_typ o TFree) goal_tfrees)
    1.26        |> fork_proof;
    1.27  
    1.28 -    val future_thm = result_ctxt |> Future.map (fn (_, x) => the_result (get_context x));
    1.29 +    val future_thm = Future.map (the_result o snd) result_ctxt;
    1.30      val finished_goal = Goal.future_result goal_ctxt future_thm prop';
    1.31      val state' =
    1.32        state
    1.33 -      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I
    1.34 -      |> done;
    1.35 -  in (Future.map #1 result_ctxt, state') end;
    1.36 -
    1.37 -in
    1.38 -
    1.39 -fun local_future_proof x = future_proof local_done_proof context_of x;
    1.40 -fun global_future_proof x = future_proof global_done_proof I x;
    1.41 +      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I;
    1.42 +  in (Future.map fst result_ctxt, state') end;
    1.43  
    1.44  end;
    1.45  
    1.46 @@ -1184,21 +1179,26 @@
    1.47  
    1.48  local
    1.49  
    1.50 -fun future_terminal_proof n proof1 proof2 meths int state =
    1.51 +fun future_terminal_proof n proof1 proof2 done int state =
    1.52    if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int)
    1.53      andalso not (is_relevant state)
    1.54    then
    1.55 -    snd (proof2 (fn state' =>
    1.56 -      Goal.fork_name "Proof.future_terminal_proof" ~1 (fn () => ((), proof1 meths state'))) state)
    1.57 -  else proof1 meths state;
    1.58 +    state |> future_proof (fn state' =>
    1.59 +      Goal.fork_name "Proof.future_terminal_proof" ~1
    1.60 +        (fn () => ((), proof2 state'))) |> snd |> done
    1.61 +  else proof1 state;
    1.62  
    1.63  in
    1.64  
    1.65 -fun local_future_terminal_proof x =
    1.66 -  future_terminal_proof 2 local_terminal_proof local_future_proof x;
    1.67 +fun local_future_terminal_proof meths =
    1.68 +  future_terminal_proof 2
    1.69 +    (local_terminal_proof meths)
    1.70 +    (local_terminal_proof meths #> context_of) local_done_proof;
    1.71  
    1.72 -fun global_future_terminal_proof x =
    1.73 -  future_terminal_proof 3 global_terminal_proof global_future_proof x;
    1.74 +fun global_future_terminal_proof meths =
    1.75 +  future_terminal_proof 3
    1.76 +    (global_terminal_proof meths)
    1.77 +    (global_terminal_proof meths) global_done_proof;
    1.78  
    1.79  end;
    1.80  
     2.1 --- a/src/Pure/Isar/toplevel.ML	Thu Feb 28 18:35:31 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Feb 28 21:11:07 2013 +0100
     2.3 @@ -746,7 +746,7 @@
     2.4          val (body_trs, end_tr) = split_last proof_trs;
     2.5          val finish = Context.Theory o Proof_Context.theory_of;
     2.6  
     2.7 -        val future_proof = Proof.global_future_proof
     2.8 +        val future_proof = Proof.future_proof
     2.9            (fn prf =>
    2.10              setmp_thread_position head_tr (fn () =>
    2.11                Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
    2.12 @@ -756,7 +756,7 @@
    2.13                        => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    2.14                      |> fold_map atom_result body_trs ||> command end_tr;
    2.15                    in (result, presentation_context_of result_state) end)) ())
    2.16 -          #-> Result.put;
    2.17 +          #> (fn (result, state') => state' |> Proof.global_done_proof |> Result.put result);
    2.18  
    2.19          val st'' = st'
    2.20            |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));