coq

Formal proof management system
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library coqide-server.core
Module Document
exception Empty
type 'a document
type id = Stateid.t
val create : unit -> 'a document
val tip : 'a document -> id

The last sentence.

  • raises Invalid_argument

    if tip has no id.

    @raise Empty

val tip_data : 'a document -> 'a

The last sentence.

  • raises Empty
val push : 'a document -> 'a -> unit

Add a sentence on the top (with no state_id)

val pop : 'a document -> 'a

Remove the tip setence.

  • raises Empty
val assign_tip_id : 'a document -> id -> unit

Assign the state_id of the tip.

  • raises Empty
val cut_at : 'a document -> id -> 'a list

cut_at d id cuts the document at id that is the new tip. Returns the list of sentences that were cut.

  • raises Not_found
val find_id : 'a document -> ( id -> 'a -> bool ) -> id * bool

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.

  • raises Not_found
val find : 'a document -> ( bool -> id option -> 'a -> bool ) -> 'a

look for a sentence validating the predicate. The boolean is true if the sentence is in the zone currently focused.

  • raises Not_found
val find_map : 'a document -> ( bool -> id option -> 'a -> 'b option ) -> 'b
val focus : 'a document -> cond_top:( id -> 'a -> bool ) -> cond_bot:( id -> 'a -> bool ) -> unit

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.

  • raises Invalid_argument

    if there is no such x and y or already focused

val unfocus : 'a document -> unit

Undoes a focus.

  • raises Invalid_argument

    "CStack.unfocus" if the stack is not focused

val focused : 'a document -> bool

Is the document focused

val is_empty : 'a document -> bool

No sentences at all

val before_tip : 'a document -> id * bool

returns the 1 to-last sentence, and true if we need to unfocus to reach it.

  • raises Not_found
val is_in_focus : 'a document -> id -> bool

Is the id in the focused zone?

val fold_all : 'a document -> 'c -> ( 'c -> bool -> id option -> 'a -> 'c ) -> 'c

Folds over the whole document starting from the topmost (maybe unfocused) sentence.

val context : 'a document -> (id * 'a) list * (id * 'a) list

Returns (top,bot) such that the document is morally (top @ s @ bot) where s is the focused part.

  • raises Invalid_argument
val print : 'a document -> ( bool -> id option -> 'a -> Pp.t ) -> Pp.t

debug print

Callbacks on documents

class type 'a signals = object ... end
val connect : 'a document -> 'a signals