diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /lib/edit.mli | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
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 |