--- a/src/Pure/Isar/isar_syn.ML Mon Nov 02 20:57:48 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Nov 02 21:03:41 2009 +0100
@@ -685,7 +685,7 @@
OuterSyntax.command "proof" "backward proof"
(K.tag_proof K.prf_block)
(Scan.option Method.parse >> (fn m => Toplevel.print o
- Toplevel.actual_proof (ProofNode.applys (Proof.proof m)) o
+ Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
Toplevel.skip_proof (fn i => i + 1)));
@@ -720,7 +720,7 @@
val _ =
OuterSyntax.command "back" "backtracking of proof command"
(K.tag_proof K.prf_script)
- (Scan.succeed (Toplevel.print o Toplevel.actual_proof ProofNode.back o Toplevel.skip_proof I));
+ (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
(* nested commands *)
--- a/src/Pure/Isar/proof_node.ML Mon Nov 02 20:57:48 2009 +0100
+++ b/src/Pure/Isar/proof_node.ML Mon Nov 02 21:03:41 2009 +0100
@@ -15,36 +15,36 @@
val apply: (Proof.state -> Proof.state) -> T -> T
end;
-structure ProofNode: PROOF_NODE =
+structure Proof_Node: PROOF_NODE =
struct
(* datatype *)
-datatype T = ProofNode of
+datatype T = Proof_Node of
(Proof.state * (*first result*)
Proof.state Seq.seq) * (*alternative results*)
int; (*linear proof position*)
-fun init st = ProofNode ((st, Seq.empty), 0);
+fun init st = Proof_Node ((st, Seq.empty), 0);
-fun current (ProofNode ((st, _), _)) = st;
-fun position (ProofNode (_, n)) = n;
+fun current (Proof_Node ((st, _), _)) = st;
+fun position (Proof_Node (_, n)) = n;
(* backtracking *)
-fun back (ProofNode ((_, stq), n)) =
+fun back (Proof_Node ((_, stq), n)) =
(case Seq.pull stq of
NONE => error "back: no alternatives"
- | SOME res => ProofNode (res, n));
+ | SOME res => Proof_Node (res, n));
(* apply transformer *)
-fun applys f (ProofNode ((st, _), n)) =
+fun applys f (Proof_Node ((st, _), n)) =
(case Seq.pull (f st) of
NONE => error "empty result sequence -- proof command failed"
- | SOME res => ProofNode (res, n + 1));
+ | SOME res => Proof_Node (res, n + 1));
fun apply f = applys (Seq.single o f);
--- a/src/Pure/Isar/toplevel.ML Mon Nov 02 20:57:48 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Nov 02 21:03:41 2009 +0100
@@ -72,7 +72,7 @@
val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
val proof: (Proof.state -> Proof.state) -> transition -> transition
- val actual_proof: (ProofNode.T -> ProofNode.T) -> transition -> transition
+ val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
val skip_proof: (int -> int) -> transition -> transition
val skip_proof_to_theory: (int -> bool) -> transition -> transition
val get_id: transition -> string option
@@ -121,7 +121,7 @@
datatype node =
Theory of generic_theory * Proof.context option
(*theory with presentation context*) |
- Proof of ProofNode.T * ((Proof.context -> generic_theory) * generic_theory)
+ Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
(*proof node, finish, original theory*) |
SkipProof of int * (generic_theory * generic_theory);
(*proof depth, resulting theory, original theory*)
@@ -130,7 +130,7 @@
val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
fun cases_node f _ (Theory (gthy, _)) = f gthy
- | cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf)
+ | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
| cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
val context_node = cases_node Context.proof_of Proof.context_of;
@@ -148,7 +148,7 @@
fun level (State (NONE, _)) = 0
| level (State (SOME (Theory _, _), _)) = 0
- | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (ProofNode.current prf)
+ | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
| level (State (SOME (SkipProof (d, _), _), _)) = d + 1; (*different notion of proof depth!*)
fun str_of_state (State (NONE, _)) = "at top level"
@@ -184,7 +184,7 @@
fun proof_position_of state =
(case node_of state of
- Proof (prf, _) => ProofNode.position prf
+ Proof (prf, _) => Proof_Node.position prf
| _ => raise UNDEF);
val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
@@ -207,7 +207,7 @@
NONE => []
| SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
| SOME (Proof (prf, _)) =>
- Proof.pretty_state (ProofNode.position prf) (ProofNode.current prf)
+ Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
| SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
|> Pretty.markup_chunks Markup.state |> Pretty.writeln;
@@ -450,7 +450,7 @@
fun end_proof f = transaction (fn int =>
(fn Proof (prf, (finish, _)) =>
- let val state = ProofNode.current prf in
+ let val state = Proof_Node.current prf in
if can (Proof.assert_bottom true) state then
let
val ctxt' = f int state;
@@ -475,7 +475,7 @@
else ();
if skip andalso not schematic then
SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
- else Proof (ProofNode.init prf, (finish gthy, gthy))
+ else Proof (Proof_Node.init prf, (finish gthy, gthy))
end
| _ => raise UNDEF));
@@ -499,12 +499,12 @@
| _ => raise UNDEF));
val present_proof = present_transaction (fn _ =>
- (fn Proof (prf, x) => Proof (ProofNode.apply I prf, x)
+ (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
| skip as SkipProof _ => skip
| _ => raise UNDEF));
fun proofs' f = transaction (fn int =>
- (fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x)
+ (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
| skip as SkipProof _ => skip
| _ => raise UNDEF));
@@ -654,7 +654,7 @@
Future.fork_pri ~1 (fn () =>
let val (states, result_state) =
(case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
- => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
+ => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev))
|> fold_map command_result body_trs
||> command (end_tr |> set_print false);
in (states, presentation_context_of result_state) end))