'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
authorwenzelm
Tue Oct 28 10:35:38 2014 +0100 (2014-10-28 ago)
changeset 5879849ed5eea15d4
parent 58797 6d71f19a9fd6
child 58799 944364b48eb9
'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Oct 28 09:57:12 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 28 10:35:38 2014 +0100
     1.3 @@ -692,7 +692,7 @@
     1.4  
     1.5  val _ =
     1.6    Outer_Syntax.command @{command_spec "oops"} "forget proof"
     1.7 -    (Scan.succeed Toplevel.forget_proof);
     1.8 +    (Scan.succeed (Toplevel.forget_proof true));
     1.9  
    1.10  
    1.11  (* proof steps *)
     2.1 --- a/src/Pure/Isar/proof.ML	Tue Oct 28 09:57:12 2014 +0100
     2.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 28 10:35:38 2014 +0100
     2.3 @@ -31,6 +31,7 @@
     2.4    val assert_backward: state -> state
     2.5    val assert_no_chain: state -> state
     2.6    val enter_forward: state -> state
     2.7 +  val has_bottom_goal: state -> bool
     2.8    val goal_message: (unit -> Pretty.T) -> state -> state
     2.9    val pretty_goal_messages: state -> Pretty.T list
    2.10    val pretty_state: int -> state -> Pretty.T list
    2.11 @@ -300,6 +301,17 @@
    2.12  val before_qed = #before_qed o #2 o current_goal;
    2.13  
    2.14  
    2.15 +(* bottom goal *)
    2.16 +
    2.17 +fun has_bottom_goal (State stack) =
    2.18 +  let
    2.19 +    fun bottom [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true
    2.20 +      | bottom [Node {goal, ...}] = is_some goal
    2.21 +      | bottom [] = false
    2.22 +      | bottom (_ :: rest) = bottom rest;
    2.23 +  in bottom (op :: (Stack.dest stack)) end;
    2.24 +
    2.25 +
    2.26  (* nested goal *)
    2.27  
    2.28  fun map_goal f g h (State stack) =
     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Oct 28 09:57:12 2014 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Oct 28 10:35:38 2014 +0100
     3.3 @@ -68,7 +68,7 @@
     3.4      (local_theory -> Proof.state) -> transition -> transition
     3.5    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
     3.6    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
     3.7 -  val forget_proof: transition -> transition
     3.8 +  val forget_proof: bool -> transition -> transition
     3.9    val present_proof: (state -> unit) -> transition -> transition
    3.10    val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
    3.11    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
    3.12 @@ -503,8 +503,10 @@
    3.13  
    3.14  end;
    3.15  
    3.16 -val forget_proof = transaction (fn _ =>
    3.17 -  (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
    3.18 +fun forget_proof strict = transaction (fn _ =>
    3.19 +  (fn Proof (prf, (_, orig_gthy)) =>
    3.20 +        if strict andalso not (Proof.has_bottom_goal (Proof_Node.current prf))
    3.21 +        then raise UNDEF else Theory (orig_gthy, NONE)
    3.22      | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
    3.23      | _ => raise UNDEF));
    3.24  
    3.25 @@ -638,7 +640,7 @@
    3.26  
    3.27  in
    3.28  
    3.29 -val reset_theory = reset_state is_theory forget_proof;
    3.30 +val reset_theory = reset_state is_theory (forget_proof false);
    3.31  
    3.32  val reset_proof =
    3.33    reset_state is_proof