src/Pure/Isar/toplevel.ML
changeset 51273 d54ee0cad2ab
parent 51268 fcc4b89a600d
child 51274 cfc83ad52571
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:17:50 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:52:27 2013 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4    val put_timing: Time.time -> transition -> transition
     1.5    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.6    val command: transition -> state -> state
     1.7 -  val proof_result: bool -> transition * transition list -> state ->
     1.8 +  val element_result: transition Thy_Syntax.element -> state ->
     1.9      (transition * state) list future * state
    1.10  end;
    1.11  
    1.12 @@ -694,10 +694,6 @@
    1.13        if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
    1.14    | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
    1.15  
    1.16 -fun command_result tr st =
    1.17 -  let val st' = command tr st
    1.18 -  in ((tr, st'), st') end;
    1.19 -
    1.20  
    1.21  (* scheduled proof result *)
    1.22  
    1.23 @@ -708,13 +704,27 @@
    1.24    fun init _ = empty;
    1.25  );
    1.26  
    1.27 -fun proof_result immediate (tr, proof_trs) st =
    1.28 -  let val st' = command tr st in
    1.29 -    if immediate orelse null proof_trs orelse not (can proof_of st') orelse
    1.30 -      Proof.is_relevant (proof_of st')
    1.31 +fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
    1.32 +  let
    1.33 +    val future_enabled = Goal.future_enabled ();
    1.34 +
    1.35 +    fun atom_result tr st =
    1.36 +      let val st' = command tr st
    1.37 +      in ((tr, st'), st') end;
    1.38 +
    1.39 +    val proof_trs =
    1.40 +      (case opt_proof of
    1.41 +        NONE => []
    1.42 +      | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
    1.43 +
    1.44 +    val st' = command head_tr st;
    1.45 +  in
    1.46 +    if not future_enabled orelse is_ignored head_tr orelse
    1.47 +      Keyword.is_schematic_goal (name_of head_tr) orelse null proof_trs orelse
    1.48 +      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
    1.49      then
    1.50 -      let val (results, st'') = fold_map command_result proof_trs st'
    1.51 -      in (Future.value ((tr, st') :: results), st'') end
    1.52 +      let val (results, st'') = fold_map atom_result proof_trs st'
    1.53 +      in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
    1.54      else
    1.55        let
    1.56          val (body_trs, end_tr) = split_last proof_trs;
    1.57 @@ -732,15 +742,15 @@
    1.58                  let val (result, result_state) =
    1.59                    (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.60                      => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.61 -                  |> fold_map command_result body_trs ||> command end_tr;
    1.62 +                  |> fold_map atom_result body_trs ||> command end_tr;
    1.63                  in (result, presentation_context_of result_state) end))
    1.64            #-> Result.put;
    1.65  
    1.66          val st'' = st'
    1.67 -          |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
    1.68 +          |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
    1.69          val result =
    1.70            Result.get (presentation_context_of st'')
    1.71 -          |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
    1.72 +          |> Future.map (fn body => (head_tr, st') :: body @ [(end_tr, st'')]);
    1.73  
    1.74        in (result, st'') end
    1.75    end;