equal
deleted
inserted
replaced
12 val init: Proof.state -> T |
12 val init: Proof.state -> T |
13 val current: T -> Proof.state |
13 val current: T -> Proof.state |
14 val clear: T -> T |
14 val clear: T -> T |
15 val undo: T -> T |
15 val undo: T -> T |
16 val redo: T -> T |
16 val redo: T -> T |
|
17 val undos: int -> T -> T |
|
18 val redos: int -> T -> T |
17 val position: T -> int |
19 val position: T -> int |
18 val nesting: T -> int |
20 val nesting: T -> int |
19 val prev: T -> T |
21 val prev: T -> T |
20 val up: T -> T |
22 val up: T -> T |
21 val top: T -> T |
23 val top: T -> T |
54 fun init st = ProofHistory (History.init (((st, Seq.empty), 0), [])); |
56 fun init st = ProofHistory (History.init (((st, Seq.empty), 0), [])); |
55 fun current (ProofHistory prf) = fst (fst (fst (History.current prf))); |
57 fun current (ProofHistory prf) = fst (fst (fst (History.current prf))); |
56 val clear = app History.clear; |
58 val clear = app History.clear; |
57 val undo = app History.undo; |
59 val undo = app History.undo; |
58 val redo = app History.redo; |
60 val redo = app History.redo; |
|
61 |
|
62 fun undos n = funpow n undo; |
|
63 fun redos n = funpow n redo; |
59 |
64 |
60 |
65 |
61 (* navigate *) |
66 (* navigate *) |
62 |
67 |
63 fun position (ProofHistory prf) = length (snd (History.current prf)); |
68 fun position (ProofHistory prf) = length (snd (History.current prf)); |