1 files changed, 56 insertions, 0 deletions
diff --git a/lib/edit.mli b/lib/edit.mli
new file mode 100644
index 00000000..edf0f67b
--- /dev/null
+++ b/lib/edit.mli
@@ -0,0 +1,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