diff options
Diffstat (limited to 'lib/edit.mli')
| -rw-r--r-- | lib/edit.mli | 63 |
1 files changed, 0 insertions, 63 deletions
diff --git a/lib/edit.mli b/lib/edit.mli deleted file mode 100644 index d3558716..00000000 --- a/lib/edit.mli +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: edit.mli 14641 2011-11-06 11:59:10Z herbelin $ 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 - -(* [depth e] Returns the depth of the focused proof stack of [e], this - is used to put informations in coq prompt (in emacs mode). *) -val depth : ('a,'b,'c) t -> int - -(* [undo_todepth e n] Undoes focused proof of [e] to reach depth [n] *) -val undo_todepth : ('a,'b,'c) t -> int -> unit |