From e0f8d741b933361fc33a4ccd683b0137c869c468 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 10 Oct 2013 11:22:52 +0000 Subject: CoqIDE: move cmd_stack to a separate module: Document The idea is to move the logic related to document handling to a separate module that can be tested by fake_ide too. CoqOps should "only" interface Document with the GtkTextBuffer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16870 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/document.mli | 126 +++++++++++++++++++++++++++++++++---------------------- 1 file changed, 75 insertions(+), 51 deletions(-) (limited to 'ide/document.mli') diff --git a/ide/document.mli b/ide/document.mli index c610f275c..556e1d022 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -6,77 +6,101 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Based on OCaml stacks, it is the structure used by CoqIDE to represent - the document *) - -type 'a t +(* An 'a document is a structure to hold and manipulate list of sentences. + Sentences are equipped with an id = Stateid.t and can carry arbitrary + data ('a). + + When added (push) to the document, a sentence has no id, it has + be manually assigned just afterward or the sentence has to be removed + (pop) before any other sentence can be pushed. + This exception is useful since the process of assigning an id to + a sentence may fail (parse error) and an error handler may want to annotate + a script buffer with the error message. This handler needs to find the + sentence in question, and it is simpler if the sentence is in the document. + Only the functions pop, find, fold_all and find_map can be called on a + document with a tip that has no id (and assign_tip_id of course). + + The document can be focused (non recursively) to a zone. After that + some functions operate on the focused zone only. When unfocused the + context (the part of the document out of focus) is restored. +*) exception Empty -(** Alias for Stack.Empty. *) - -val create : unit -> 'a t -(** Create an empty stack. *) -val push : 'a -> 'a t -> unit -(** Add an element to a stack. *) +type 'a document +type id = Stateid.t -val find : ('a -> bool -> bool) -> 'a t -> 'a -(** Find the first element satisfying the predicate. - The boolean tells If the element is inside the focused zone. - @raise Not_found it there is none. *) +val create : unit -> 'a document -val is_empty : 'a t -> bool -(** Whether a stack is empty. *) +(* Functions that work on the focused part of the document ******************* *) -val iter : ('a -> bool -> unit) -> 'a t -> unit -(** Iterate a function over elements, from the last added one. - The boolean tells If the element is inside the focused zone. *) +(** The last sentence. @raise Invalid_argument if tip has no id. @raise Empty *) +val tip : 'a document -> id -val clear : 'a t -> unit -(** Empty a stack. *) +(** The last sentence. @raise Empty *) +val tip_data : 'a document -> 'a -val length : 'a t -> int -(** Length of a stack. *) +(** Add a sentence on the top (with no state_id) *) +val push : 'a document -> 'a -> unit -val pop : 'a t -> 'a -(** Remove and returns the first element of the stack. - @raise Empty if empty. *) +(** Remove the tip setence. @raise Empty *) +val pop : 'a document -> 'a -val tip : 'a t -> 'a -(** Remove the first element of the stack without modifying it. - @raise Empty if empty. *) +(** Assign the state_id of the tip. @raise Empty *) +val assign_tip_id : 'a document -> id -> unit -val to_list : 'a t -> 'a list -(** Convert to a list. *) +(** [cut_at d id] cuts the document at [id] that is the new tip. + Returns the list of sentences that were cut. + @raise Not_found *) +val cut_at : 'a document -> id -> 'a list -val find_map : ('a -> bool -> 'b option) -> 'a t -> 'b -(** Find the first element that returns [Some _]. - The boolean tells If the element is inside the focused zone. - @raise Not_found it there is none. *) +(* Functions that work on the whole document ********************************* *) -type ('b, 'c) seek = ('b, 'c) CSig.seek = Stop of 'b | Next of 'c +(** returns the id of the topmost sentence validating the predicate and + a boolean that is true if one needs to unfocus the document to access + such sentence. @raise Not_found *) +val find_id : 'a document -> (id -> 'a -> bool) -> id * bool -(** [seek f acc s] acts like [List.fold_left f acc s] while [f] returns - [Next acc']; it stops returning [b] as soon as [f] returns [Stop b]. - The stack is traversed from the top and is not altered. - @raise Not_found it there is none. *) -val fold_until : ('c -> 'a -> ('b, 'c) seek) -> 'c -> 'a t -> 'b +(** look for a sentence validating the predicate. The boolean is true + if the sentence is in the zone currently focused. @raise Not_found *) +val find : 'a document -> (bool -> id option -> 'a -> bool) -> 'a +val find_map : 'a document -> (bool -> id option -> 'a -> 'b option) -> 'b (** After [focus s c1 c2] the top of [s] is the topmost element [x] such that [c1 x] is [true] and the bottom is the first element [y] following [x] - such that [c2 y] is [true]. After a focus push/pop/top/fold_until - only use the focused part. - @raise Invalid_argument "CStack.focus" if there is no such [x] and [y] *) -val focus : 'a t -> cond_top:('a -> bool) -> cond_bot:('a -> bool) -> unit + such that [c2 y] is [true]. + @raise Invalid_argument if there is no such [x] and [y] or already focused *) +val focus : + 'a document -> + cond_top:(id -> 'a -> bool) -> cond_bot:(id -> 'a -> bool) -> unit (** Undoes a [focus]. @raise Invalid_argument "CStack.unfocus" if the stack is not focused *) -val unfocus : 'a t -> unit +val unfocus : 'a document -> unit + +(** Is the document focused *) +val focused : 'a document -> bool + +(** No sentences at all *) +val is_empty : 'a document -> bool + +(** returns the 1 to-last sentence, and true if we need to unfocus to reach it. + @raise Not_found *) +val before_tip : 'a document -> id * bool + +(** Is the id in the focused zone? *) +val is_in_focus : 'a document -> id -> bool + +(** Folds over the whole document starting from the topmost (maybe unfocused) + sentence. *) +val fold_all : + 'a document -> 'c -> ('c -> bool -> id option -> 'a -> 'c) -> 'c -(** Is the stack focused *) -val focused : 'a t -> bool +(** Returns (top,bot) such that the document is morally (top @ s @ bot) where + s is the focused part. @raise Invalid_argument *) +val context : 'a document -> (id * 'a) list * (id * 'a) list -(** Returns [top, s, bot] where [top @ s @ bot] is the full stack, and [s] - the focused part *) -val to_lists : 'a t -> 'a list * 'a list * 'a list +(** debug print *) +val print : + 'a document -> (bool -> id option -> 'a -> Pp.std_ppcmds) -> Pp.std_ppcmds -- cgit v1.2.3