equal
deleted
inserted
replaced
11 exception FAIL of string |
11 exception FAIL of string |
12 val position: T -> int |
12 val position: T -> int |
13 val init: int option -> Proof.state -> T |
13 val init: int option -> Proof.state -> T |
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 previous: T -> Proof.state option |
16 val clear: int -> T -> T |
17 val clear: int -> T -> T |
17 val undo: T -> T |
18 val undo: T -> T |
18 val redo: T -> T |
19 val redo: T -> T |
19 val back: bool -> T -> T |
20 val back: bool -> T -> T |
20 val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T |
21 val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T |
46 (* generic history operations *) |
47 (* generic history operations *) |
47 |
48 |
48 fun init lim st = ProofHistory (History.init lim ((st, Seq.empty), [])); |
49 fun init lim st = ProofHistory (History.init lim ((st, Seq.empty), [])); |
49 fun is_initial (ProofHistory prf) = History.is_initial prf; |
50 fun is_initial (ProofHistory prf) = History.is_initial prf; |
50 fun current (ProofHistory prf) = fst (fst (History.current prf)); |
51 fun current (ProofHistory prf) = fst (fst (History.current prf)); |
|
52 fun previous (ProofHistory prf) = Option.map (fst o fst) (History.previous prf); |
51 val clear = app o History.clear; |
53 val clear = app o History.clear; |
52 val undo = app History.undo; |
54 val undo = app History.undo; |
53 val redo = app History.redo; |
55 val redo = app History.redo; |
54 |
56 |
55 |
57 |