# 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;