# HG changeset patch
# User wenzelm
# Date 1414488938 -3600
# Node ID 49ed5eea15d48bef6d66945901648f9344219141
# Parent  6d71f19a9fd69e3dfbf2cde819da24ceac1fd664
'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;

diff -r 6d71f19a9fd6 -r 49ed5eea15d4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 28 09:57:12 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 28 10:35:38 2014 +0100
@@ -692,7 +692,7 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "oops"} "forget proof"
-    (Scan.succeed Toplevel.forget_proof);
+    (Scan.succeed (Toplevel.forget_proof true));
 
 
 (* proof steps *)
diff -r 6d71f19a9fd6 -r 49ed5eea15d4 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Oct 28 09:57:12 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Oct 28 10:35:38 2014 +0100
@@ -31,6 +31,7 @@
   val assert_backward: state -> state
   val assert_no_chain: state -> state
   val enter_forward: state -> state
+  val has_bottom_goal: state -> bool
   val goal_message: (unit -> Pretty.T) -> state -> state
   val pretty_goal_messages: state -> Pretty.T list
   val pretty_state: int -> state -> Pretty.T list
@@ -300,6 +301,17 @@
 val before_qed = #before_qed o #2 o current_goal;
 
 
+(* bottom goal *)
+
+fun has_bottom_goal (State stack) =
+  let
+    fun bottom [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true
+      | bottom [Node {goal, ...}] = is_some goal
+      | bottom [] = false
+      | bottom (_ :: rest) = bottom rest;
+  in bottom (op :: (Stack.dest stack)) end;
+
+
 (* nested goal *)
 
 fun map_goal f g h (State stack) =
diff -r 6d71f19a9fd6 -r 49ed5eea15d4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Oct 28 09:57:12 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 28 10:35:38 2014 +0100
@@ -68,7 +68,7 @@
     (local_theory -> Proof.state) -> transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
-  val forget_proof: transition -> transition
+  val forget_proof: bool -> transition -> transition
   val present_proof: (state -> unit) -> transition -> transition
   val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
@@ -503,8 +503,10 @@
 
 end;
 
-val forget_proof = transaction (fn _ =>
-  (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
+fun forget_proof strict = transaction (fn _ =>
+  (fn Proof (prf, (_, orig_gthy)) =>
+        if strict andalso not (Proof.has_bottom_goal (Proof_Node.current prf))
+        then raise UNDEF else Theory (orig_gthy, NONE)
     | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
     | _ => raise UNDEF));
 
@@ -638,7 +640,7 @@
 
 in
 
-val reset_theory = reset_state is_theory forget_proof;
+val reset_theory = reset_state is_theory (forget_proof false);
 
 val reset_proof =
   reset_state is_proof