5039
|
1 |
(* Title: Pure/General/history.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
|
5 |
Histories of values, with undo and redo.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature HISTORY =
|
|
9 |
sig
|
|
10 |
type 'a T
|
|
11 |
val init: 'a -> 'a T
|
|
12 |
val current: 'a T -> 'a
|
|
13 |
val clear: 'a T -> 'a T
|
|
14 |
val undo: 'a T -> 'a T
|
|
15 |
val redo: 'a T -> 'a T
|
|
16 |
val apply: ('a -> 'a) -> 'a T -> 'a T
|
|
17 |
end;
|
|
18 |
|
|
19 |
structure History: HISTORY =
|
|
20 |
struct
|
|
21 |
|
|
22 |
|
|
23 |
(* datatype history *)
|
|
24 |
|
|
25 |
datatype 'a T =
|
|
26 |
History of 'a * 'a list * 'a list;
|
|
27 |
|
|
28 |
fun init x = History (x, [], []);
|
|
29 |
|
|
30 |
fun current (History (x, _, _)) = x;
|
|
31 |
|
|
32 |
fun clear (History (x, _, _)) = History (x, [], []);
|
|
33 |
|
|
34 |
fun undo (History (_, [], _)) = error "No further undo information"
|
|
35 |
| undo (History (x, u :: undo_list, redo_list)) = History (u, undo_list, x :: redo_list);
|
|
36 |
|
|
37 |
fun redo (History (_, _, [])) = error "No further redo information"
|
|
38 |
| redo (History (x, undo_list, r :: redo_list)) = History (r, x :: undo_list, redo_list);
|
|
39 |
|
|
40 |
fun apply f (History (x, undo_list, _)) =
|
|
41 |
History (f x, x :: undo_list, []);
|
|
42 |
|
|
43 |
|
|
44 |
end;
|