src/Pure/Isar/proof_history.ML
changeset 7366 22a64baa7013
parent 6902 5f126c495771
child 7731 51d59734743d
equal deleted inserted replaced
7365:b5bb32e0861c 7366:22a64baa7013
    14   val is_initial: T -> bool
    14   val is_initial: T -> bool
    15   val current: T -> Proof.state
    15   val current: T -> Proof.state
    16   val clear: T -> T
    16   val clear: T -> T
    17   val undo: T -> T
    17   val undo: T -> T
    18   val redo: T -> T
    18   val redo: T -> T
    19   val back: T -> T
    19   val back: bool -> T -> T
    20   val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
    20   val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
    21   val apply: (Proof.state -> Proof.state) -> T -> T
    21   val apply: (Proof.state -> Proof.state) -> T -> T
    22 end;
    22 end;
    23 
    23 
    24 structure ProofHistory: PROOF_HISTORY =
    24 structure ProofHistory: PROOF_HISTORY =
    53 val redo = app History.redo;
    53 val redo = app History.redo;
    54 
    54 
    55 
    55 
    56 (* backtrack *)
    56 (* backtrack *)
    57 
    57 
    58 fun back_fun ((_, stq), nodes) =
    58 fun back_fun recur ((_, stq), nodes) =
    59   (case Seq.pull stq of
    59   (case Seq.pull stq of
    60     None =>
    60     None =>
    61       (case nodes of
    61       if recur andalso not (null nodes) then
    62         [] => raise FAIL "back: no alternatives"
    62         (writeln "back: trying previous proof state ..."; back_fun recur (hd nodes, tl nodes))
    63       | nd :: nds => (writeln "back: trying previous proof state ..."; back_fun (nd, nds)))
    63       else raise FAIL "back: no alternatives"
    64   | Some result => (result, nodes));
    64   | Some result => (result, nodes));
    65 
    65 
    66 val back = hist_app back_fun;
    66 val back = hist_app o back_fun;
    67 
    67 
    68 
    68 
    69 (* apply transformer *)
    69 (* apply transformer *)
    70 
    70 
    71 fun applys f = hist_app (fn (node as (st, _), nodes) =>
    71 fun applys f = hist_app (fn (node as (st, _), nodes) =>