src/Pure/Isar/proof_history.ML
changeset 16490 e10b0d5fa33a
parent 15531 08c8dad8e399
child 16814 b829a6c9a87a
equal deleted inserted replaced
16489:f66ab8a4e98f 16490:e10b0d5fa33a
     1 (*  Title:      Pure/Isar/proof_history.ML
     1 (*  Title:      Pure/Isar/proof_history.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     4 
     5 Histories of proof states, with undo / redo and prev / back.
     5 Histories of proof states, with undo / redo and backtracking.
     6 *)
     6 *)
     7 
     7 
     8 signature PROOF_HISTORY =
     8 signature PROOF_HISTORY =
     9 sig
     9 sig
    10   type T
    10   type T
    26 
    26 
    27 
    27 
    28 (* datatype proof history *)
    28 (* datatype proof history *)
    29 
    29 
    30 type node =
    30 type node =
    31   Proof.state *			(*first result*)
    31   Proof.state *                 (*first result*)
    32   Proof.state Seq.seq; 		(*alternative results*)
    32   Proof.state Seq.seq;          (*alternative results*)
    33 
    33 
    34 type proof = node * node list;
    34 type proof = node * node list;
    35 
    35 
    36 datatype T = ProofHistory of proof History.T;
    36 datatype T = ProofHistory of proof History.T;
    37 
    37 
    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 recur ((_, stq), nodes) =
    58 fun backtrack recur ((_, stq), nodes) =
    59   (case Seq.pull stq of
    59   (case Seq.pull stq of
    60     NONE =>
    60     NONE =>
    61       if recur andalso not (null nodes) then
    61       if recur andalso not (null nodes) then
    62         (writeln "back: trying previous proof state ..."; back_fun recur (hd nodes, tl nodes))
    62         (writeln "back: trying previous proof state ..."; backtrack recur (hd nodes, tl nodes))
    63       else raise FAIL "back: no alternatives"
    63       else raise FAIL "back: no alternatives"
    64   | SOME result => (result, nodes));
    64   | SOME result => (result, nodes));
    65 
    65 
    66 val back = hist_app o back_fun;
    66 val back = hist_app o backtrack;
    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) =>