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 48 49 50 51 52 53 54 55 56
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: edit.mli,v 1.5.2.1 2004/07/16 19:30:29 herbelin Exp $ i*)
(* 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 *)
val focus : ('a,'b,'c) t -> 'a -> unit
(* unsets the focus which must not already be unfocused *)
val unfocus : ('a,'b,'c) t -> 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 -> unit
val delete : ('a,'b,'c) t -> 'a -> unit
val dom : ('a,'b,'c) t -> 'a list
val clear : ('a,'b,'c) t -> unit
|