aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/edit.mli
blob: 6d5744259d55f4ce590540935527c9527171249e (plain)
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