1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
(* $Id$ *)
(* The type of editors.
* An editor is a finite map, ['a -> 'b], which knows how to apply
* modification functions to the value in the range, and how to
* focus on a member of the range.
* It also supports the notion of a limited-depth undo, and that certain
* modification actions do not push onto the undo stack, since they are
* reversible. *)
type ('a,'b,'c) t
val empty : unit -> ('a,'b,'c) t
(* sets the focus to the specified domain element, or if [None],
* unsets the focus *)
val focus : ('a,'b,'c) t -> 'a option -> unit
(* gives the last focused element or [None] if none *)
val last_focused : ('a,'b,'c) t -> 'a option
(* are we focused ? *)
val focusedp : ('a,'b,'c) t -> bool
(* If we are focused, then return the current domain,range pair. *)
val read : ('a,'b,'c) t -> ('a * 'b * 'c) option
(* mutates the currently-focused range element, pushing its
* old value onto the undo stack
*)
val mutate : ('a,'b,'c) t -> ('c -> 'b -> 'b) -> unit
(* mutates the currently-focused range element, in place. *)
val rev_mutate : ('a,'b,'c) t -> ('c -> 'b -> 'b) -> unit
(* Pops the specified number of elements off of the undo stack, *
reinstating the last popped element. The undo stack is independently
managed for each range element. *)
val undo : ('a,'b,'c) t -> int -> unit
val create : ('a,'b,'c) t -> 'a * 'b * 'c * int option -> unit
val delete : ('a,'b,'c) t -> 'a -> unit
val dom : ('a,'b,'c) t -> 'a list
val clear : ('a,'b,'c) t -> unit
|
