uniform treatment of global/local proofs;
authorwenzelm
Sun Mar 03 14:29:30 2013 +0100 (2013-03-03 ago)
changeset 51324c17f5de0a915
parent 51323 1b37556a3644
child 51325 bcd6b1aa4db5
uniform treatment of global/local proofs;
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Mar 03 13:57:03 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Mar 03 14:29:30 2013 +0100
     1.3 @@ -714,6 +714,20 @@
     1.4    fun init _ = empty;
     1.5  );
     1.6  
     1.7 +fun done_proof state =
     1.8 +  if can (Proof.assert_bottom true) state
     1.9 +  then Proof.global_done_proof state
    1.10 +  else Proof.context_of (Proof.local_done_proof state);
    1.11 +
    1.12 +fun proof_future_enabled st =
    1.13 +  (case try proof_of st of
    1.14 +    NONE => false
    1.15 +  | SOME state =>
    1.16 +      not (Proof.is_relevant state) andalso
    1.17 +       (if can (Proof.assert_bottom true) state
    1.18 +        then Goal.future_enabled ()
    1.19 +        else Goal.future_enabled_nested 2));
    1.20 +
    1.21  fun priority elem =
    1.22    let
    1.23      val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem Time.zeroTime;
    1.24 @@ -734,46 +748,44 @@
    1.25  
    1.26  in
    1.27  
    1.28 -fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
    1.29 -  let
    1.30 -    val proof_trs =
    1.31 -      (case opt_proof of
    1.32 -        NONE => []
    1.33 -      | SOME (a, b) => maps Thy_Syntax.flat_element a @ [b]);
    1.34 -
    1.35 -    val (_, st') = atom_result head_tr st;
    1.36 -  in
    1.37 -    if not (Goal.future_enabled ()) orelse null proof_trs orelse
    1.38 -      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
    1.39 -    then
    1.40 -      let val (results, st'') = fold_map atom_result proof_trs st'
    1.41 -      in (Future.value ((head_tr, st') :: results), st'') end
    1.42 -    else
    1.43 +fun element_result (Thy_Syntax.Element (tr, NONE)) st =
    1.44 +      let val (result, st') = atom_result tr st
    1.45 +      in (Future.value [result], st') end
    1.46 +  | element_result (Thy_Syntax.Element (head_tr, SOME proof)) st =
    1.47        let
    1.48 -        val (body_trs, end_tr) = split_last proof_trs;
    1.49 -        val finish = Context.Theory o Proof_Context.theory_of;
    1.50 +        val (head_result, st') = atom_result head_tr st;
    1.51 +        val (body_elems, end_tr) = proof;
    1.52 +        val body_trs = maps Thy_Syntax.flat_element body_elems;
    1.53 +      in
    1.54 +        if not (proof_future_enabled st')
    1.55 +        then
    1.56 +          let val (proof_results, st'') = fold_map atom_result (body_trs @ [end_tr]) st'
    1.57 +          in (Future.value (head_result :: proof_results), st'') end
    1.58 +        else
    1.59 +          let
    1.60 +            val finish = Context.Theory o Proof_Context.theory_of;
    1.61  
    1.62 -        val future_proof = Proof.future_proof
    1.63 -          (fn prf =>
    1.64 -            setmp_thread_position head_tr (fn () =>
    1.65 -              Goal.fork_name "Toplevel.future_proof"
    1.66 -                (priority (Thy_Syntax.Element (empty, opt_proof)))
    1.67 -                (fn () =>
    1.68 -                  let val (result, result_state) =
    1.69 -                    (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.70 -                      => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.71 -                    |> fold_map atom_result body_trs ||> command end_tr;
    1.72 -                  in (result, presentation_context_of result_state) end)) ())
    1.73 -          #> (fn (result, state') => state' |> Proof.global_done_proof |> Result.put result);
    1.74 +            val future_proof = Proof.future_proof
    1.75 +              (fn prf =>
    1.76 +                setmp_thread_position head_tr (fn () =>
    1.77 +                  Goal.fork_name "Toplevel.future_proof"
    1.78 +                    (priority (Thy_Syntax.Element (empty, SOME proof)))
    1.79 +                    (fn () =>
    1.80 +                      let val (result, result_state) =
    1.81 +                        (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.82 +                          => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.83 +                        |> fold_map atom_result body_trs ||> command end_tr;
    1.84 +                      in (result, presentation_context_of result_state) end)) ())
    1.85 +              #> (fn (result, state') => state' |> done_proof |> Result.put result);
    1.86  
    1.87 -        val st'' = st'
    1.88 -          |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
    1.89 -        val result =
    1.90 -          Result.get (presentation_context_of st'')
    1.91 -          |> Future.map (fn body => (head_tr, st') :: body @ [(end_tr, st'')]);
    1.92 +            val st'' = st'
    1.93 +              |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
    1.94 +            val result =
    1.95 +              Result.get (presentation_context_of st'')
    1.96 +              |> Future.map (fn body_results => head_result :: body_results @ [(end_tr, st'')]);
    1.97  
    1.98 -      in (result, st'') end
    1.99 -  end;
   1.100 +          in (result, st'') end
   1.101 +      end;
   1.102  
   1.103  end;
   1.104