# HG changeset patch
# User wenzelm
# Date 931287877 -7200
# Node ID 5f126c4957712d678cd33555278a09341f7c6514
# Parent  5e20ddfdf3c7a53e760b9b6f0da214521879ddeb
removed nesting (unused);

diff -r 5e20ddfdf3c7 -r 5f126c495771 src/Pure/Isar/proof_history.ML
--- a/src/Pure/Isar/proof_history.ML	Tue Jul 06 21:03:57 1999 +0200
+++ b/src/Pure/Isar/proof_history.ML	Tue Jul 06 21:04:37 1999 +0200
@@ -9,25 +9,16 @@
 sig
   type T
   exception FAIL of string
+  val position: T -> int
   val init: int option -> Proof.state -> T
   val is_initial: T -> bool
   val current: T -> Proof.state
   val clear: T -> T
   val undo: T -> T
   val redo: T -> T
-  val position: T -> int
-  val nesting: T -> int
-  val prev: T -> T
-  val up: T -> T
-  val top: T -> T
   val back: T -> T
   val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
-  val applys_open: (Proof.state -> Proof.state Seq.seq) -> T -> T
-  val applys_close: (Proof.state -> Proof.state Seq.seq) -> T -> T
   val apply: (Proof.state -> Proof.state) -> T -> T
-  val apply_open: (Proof.state -> Proof.state) -> T -> T
-  val apply_close: (Proof.state -> Proof.state) -> T -> T
-  val apply_cond_open: bool -> (Proof.state -> Proof.state) -> T -> T
 end;
 
 structure ProofHistory: PROOF_HISTORY =
@@ -37,9 +28,8 @@
 (* datatype proof history *)
 
 type node =
- (Proof.state *			(*first result*)
-  Proof.state Seq.seq) *	(*alternative results*)
-  int;				(*nest level*)
+  Proof.state *			(*first result*)
+  Proof.state Seq.seq; 		(*alternative results*)
 
 type proof = node * node list;
 
@@ -50,59 +40,40 @@
 fun app f (ProofHistory x) = ProofHistory (f x);
 fun hist_app f = app (History.apply f);
 
+fun position (ProofHistory prf) = length (snd (History.current prf));
+
 
 (* generic history operations *)
 
-fun init lim st = ProofHistory (History.init lim (((st, Seq.empty), 0), []));
+fun init lim st = ProofHistory (History.init lim ((st, Seq.empty), []));
 fun is_initial (ProofHistory prf) = History.is_initial prf;
-fun current (ProofHistory prf) = fst (fst (fst (History.current prf)));
+fun current (ProofHistory prf) = fst (fst (History.current prf));
 val clear = app History.clear;
 val undo = app History.undo;
 val redo = app History.redo;
 
 
-(* navigate *)
-
-fun position (ProofHistory prf) = length (snd (History.current prf));
-fun nesting (ProofHistory prf) = snd (fst (History.current prf));
-
-fun prev_until msg _ (_, []) = raise FAIL msg
-  | prev_until msg pred (_, node :: nodes) =
-      if pred node then (node, nodes)
-      else prev_until msg pred (node, nodes);
-
-val prev = hist_app (prev_until "no previous proof state" (K true));
-fun up prf = hist_app (prev_until "no upper proof state" (fn (_, m) => m < nesting prf)) prf;
-val top = hist_app (fn (node, nodes) => (last_elem (node :: nodes), []));
-
-
 (* backtrack *)
 
-fun back_fun (((_, stq), n), nodes) =
+fun back_fun ((_, stq), nodes) =
   (case Seq.pull stq of
     None =>
       (case nodes of
         [] => raise FAIL "back: no alternatives"
       | nd :: nds => (writeln "back: trying previous proof state ..."; back_fun (nd, nds)))
-  | Some result => ((result, n), nodes));
+  | Some result => (result, nodes));
 
 val back = hist_app back_fun;
 
 
 (* apply transformer *)
 
-fun gen_apply d f (node as ((st, _), n): node, nodes) =
+fun applys f = hist_app (fn (node as (st, _), nodes) =>
   (case Seq.pull (f st) of
-    None => raise FAIL "empty result sequence -- command failed"
-  | Some results => ((results, n + d), node :: nodes));
-
-val applys = hist_app o gen_apply 0;
-val applys_open = hist_app o gen_apply 1;
-val applys_close = hist_app o gen_apply ~1;
+    None => raise FAIL "empty result sequence -- proof command failed"
+  | Some results => (results, node :: nodes)));
 
 fun apply f = applys (Seq.single o f);
-fun apply_open f = applys_open (Seq.single o f);
-fun apply_close f = applys_close (Seq.single o f);
-fun apply_cond_open do_open f = if do_open then apply_open f else apply f;
+
 
 end;