module Bstack et Edit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@87 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 47 insertions, 0 deletions

diff --git a/lib/edit.mli b/lib/edit.mli
new file mode 100644
index 0000000000..6d5744259d
--- /dev/null
+++ b/lib/edit.mli
@@ -0,0 +1,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