src/Pure/Isar/toplevel.ML

--- a/src/Pure/Isar/toplevel.ML	Wed Mar 27 16:46:52 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 27 17:53:29 2013 +0100
@@ -12,6 +12,7 @@
   val is_toplevel: state -> bool
   val is_theory: state -> bool
   val is_proof: state -> bool
+  val is_skipped_proof: state -> bool
   val level: state -> int
   val presentation_context_of: state -> Proof.context
   val previous_context_of: state -> Proof.context option
@@ -128,15 +129,16 @@
     (*theory with presentation context*) |
   Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
     (*proof node, finish, original theory*) |
-  SkipProof of int * (generic_theory * generic_theory);
+  Skipped_Proof of int * (generic_theory * generic_theory);
     (*proof depth, resulting theory, original theory*)
 
 val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
 val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
+val skipped_proof_node = fn Skipped_Proof _ => true | _ => false;
 
 fun cases_node f _ (Theory (gthy, _)) = f gthy
   | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
-  | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
+  | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy;
 
 val context_node = cases_node Context.proof_of Proof.context_of;
 
@@ -153,13 +155,13 @@
 fun level (State (NONE, _)) = 0
   | level (State (SOME (Theory _), _)) = 0
   | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
-  | level (State (SOME (SkipProof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
+  | level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
 
 fun str_of_state (State (NONE, _)) = "at top level"
   | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
   | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
   | str_of_state (State (SOME (Proof _), _)) = "in proof mode"
-  | str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode";
+  | str_of_state (State (SOME (Skipped_Proof _), _)) = "in skipped proof mode";
 
 
 (* current node *)
@@ -169,6 +171,7 @@
 
 fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
 fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
+fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state);
 
 fun node_case f g state = cases_node f g (node_of state);
 
@@ -205,7 +208,7 @@
     NONE => []
   | SOME (Theory (gthy, _)) => pretty_context gthy
   | SOME (Proof (_, (_, gthy))) => pretty_context gthy
-  | SOME (SkipProof (_, (gthy, _))) => pretty_context gthy)
+  | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy)
   |> Pretty.chunks |> Pretty.writeln;
 
 fun print_state prf_only state =
@@ -214,7 +217,7 @@
   | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
   | SOME (Proof (prf, _)) =>
       Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
-  | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
+  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
   |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
 
 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
@@ -511,7 +514,7 @@
             in Theory (gthy', SOME ctxt') end
           else raise UNDEF
         end
-    | SkipProof (0, (gthy, _)) => Theory (gthy, NONE)
+    | Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE)
     | _ => raise UNDEF));
 
 local
@@ -529,7 +532,7 @@
         else ();
     in
       if skip andalso not no_skip then
-        SkipProof (0, (finish (Proof.global_skip_proof true prf), gthy))
+        Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy))
       else Proof (Proof_Node.init prf, (finish, gthy))
     end
   | _ => raise UNDEF));
@@ -554,17 +557,17 @@
 
 val forget_proof = transaction (fn _ =>
   (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
-    | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
+    | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
     | _ => raise UNDEF));
 
 val present_proof = present_transaction (fn _ =>
   (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
-    | skip as SkipProof _ => skip
+    | skip as Skipped_Proof _ => skip
     | _ => raise UNDEF));
 
 fun proofs' f = transaction (fn int =>
   (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
-    | skip as SkipProof _ => skip
+    | skip as Skipped_Proof _ => skip
     | _ => raise UNDEF));
 
 fun proof' f = proofs' ((Seq.single o Seq.Result) oo f);
@@ -576,11 +579,11 @@
     | _ => raise UNDEF));
 
 fun skip_proof f = transaction (fn _ =>
-  (fn SkipProof (h, x) => SkipProof (f h, x)
+  (fn Skipped_Proof (h, x) => Skipped_Proof (f h, x)
     | _ => raise UNDEF));
 
 fun skip_proof_to_theory pred = transaction (fn _ =>
-  (fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
+  (fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
     | _ => raise UNDEF));