explicit Toplevel.is_skipped_proof;
authorwenzelm
Wed Mar 27 17:53:29 2013 +0100 (2013-03-27 ago)
changeset 515556aa64925db77
parent 51554 041bc3d31f23
child 51556 7ada6dfa9ab5
explicit Toplevel.is_skipped_proof;
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 27 16:46:52 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 27 17:53:29 2013 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4    val is_toplevel: state -> bool
     1.5    val is_theory: state -> bool
     1.6    val is_proof: state -> bool
     1.7 +  val is_skipped_proof: state -> bool
     1.8    val level: state -> int
     1.9    val presentation_context_of: state -> Proof.context
    1.10    val previous_context_of: state -> Proof.context option
    1.11 @@ -128,15 +129,16 @@
    1.12      (*theory with presentation context*) |
    1.13    Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
    1.14      (*proof node, finish, original theory*) |
    1.15 -  SkipProof of int * (generic_theory * generic_theory);
    1.16 +  Skipped_Proof of int * (generic_theory * generic_theory);
    1.17      (*proof depth, resulting theory, original theory*)
    1.18  
    1.19  val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
    1.20  val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
    1.21 +val skipped_proof_node = fn Skipped_Proof _ => true | _ => false;
    1.22  
    1.23  fun cases_node f _ (Theory (gthy, _)) = f gthy
    1.24    | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
    1.25 -  | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
    1.26 +  | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy;
    1.27  
    1.28  val context_node = cases_node Context.proof_of Proof.context_of;
    1.29  
    1.30 @@ -153,13 +155,13 @@
    1.31  fun level (State (NONE, _)) = 0
    1.32    | level (State (SOME (Theory _), _)) = 0
    1.33    | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
    1.34 -  | level (State (SOME (SkipProof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
    1.35 +  | level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
    1.36  
    1.37  fun str_of_state (State (NONE, _)) = "at top level"
    1.38    | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
    1.39    | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
    1.40    | str_of_state (State (SOME (Proof _), _)) = "in proof mode"
    1.41 -  | str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode";
    1.42 +  | str_of_state (State (SOME (Skipped_Proof _), _)) = "in skipped proof mode";
    1.43  
    1.44  
    1.45  (* current node *)
    1.46 @@ -169,6 +171,7 @@
    1.47  
    1.48  fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
    1.49  fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
    1.50 +fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state);
    1.51  
    1.52  fun node_case f g state = cases_node f g (node_of state);
    1.53  
    1.54 @@ -205,7 +208,7 @@
    1.55      NONE => []
    1.56    | SOME (Theory (gthy, _)) => pretty_context gthy
    1.57    | SOME (Proof (_, (_, gthy))) => pretty_context gthy
    1.58 -  | SOME (SkipProof (_, (gthy, _))) => pretty_context gthy)
    1.59 +  | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy)
    1.60    |> Pretty.chunks |> Pretty.writeln;
    1.61  
    1.62  fun print_state prf_only state =
    1.63 @@ -214,7 +217,7 @@
    1.64    | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
    1.65    | SOME (Proof (prf, _)) =>
    1.66        Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
    1.67 -  | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
    1.68 +  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
    1.69    |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
    1.70  
    1.71  fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
    1.72 @@ -511,7 +514,7 @@
    1.73              in Theory (gthy', SOME ctxt') end
    1.74            else raise UNDEF
    1.75          end
    1.76 -    | SkipProof (0, (gthy, _)) => Theory (gthy, NONE)
    1.77 +    | Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE)
    1.78      | _ => raise UNDEF));
    1.79  
    1.80  local
    1.81 @@ -529,7 +532,7 @@
    1.82          else ();
    1.83      in
    1.84        if skip andalso not no_skip then
    1.85 -        SkipProof (0, (finish (Proof.global_skip_proof true prf), gthy))
    1.86 +        Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy))
    1.87        else Proof (Proof_Node.init prf, (finish, gthy))
    1.88      end
    1.89    | _ => raise UNDEF));
    1.90 @@ -554,17 +557,17 @@
    1.91  
    1.92  val forget_proof = transaction (fn _ =>
    1.93    (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
    1.94 -    | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
    1.95 +    | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
    1.96      | _ => raise UNDEF));
    1.97  
    1.98  val present_proof = present_transaction (fn _ =>
    1.99    (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
   1.100 -    | skip as SkipProof _ => skip
   1.101 +    | skip as Skipped_Proof _ => skip
   1.102      | _ => raise UNDEF));
   1.103  
   1.104  fun proofs' f = transaction (fn int =>
   1.105    (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
   1.106 -    | skip as SkipProof _ => skip
   1.107 +    | skip as Skipped_Proof _ => skip
   1.108      | _ => raise UNDEF));
   1.109  
   1.110  fun proof' f = proofs' ((Seq.single o Seq.Result) oo f);
   1.111 @@ -576,11 +579,11 @@
   1.112      | _ => raise UNDEF));
   1.113  
   1.114  fun skip_proof f = transaction (fn _ =>
   1.115 -  (fn SkipProof (h, x) => SkipProof (f h, x)
   1.116 +  (fn Skipped_Proof (h, x) => Skipped_Proof (f h, x)
   1.117      | _ => raise UNDEF));
   1.118  
   1.119  fun skip_proof_to_theory pred = transaction (fn _ =>
   1.120 -  (fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
   1.121 +  (fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
   1.122      | _ => raise UNDEF));
   1.123  
   1.124