package coqide-server

  1. Overview
  2. Docs
The Coq Proof Assistant, XML protocol server

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

doc/coqide-server.core/Document/index.html

Module DocumentSource

Sourceexception Empty
Sourcetype 'a document
Sourcetype id = Stateid.t
Sourceval create : unit -> 'a document
Sourceval tip : 'a document -> id

The last sentence.

Sourceval tip_data : 'a document -> 'a

The last sentence.

Sourceval push : 'a document -> 'a -> unit

Add a sentence on the top (with no state_id)

Sourceval pop : 'a document -> 'a

Remove the tip setence.

Sourceval set_errors : 'a document -> string list -> unit

preserve the last error(s) (tooltip fix)

Sourceval get_errors : 'a document -> string list

get the last error(s) (tooltip fix)

Sourceval assign_tip_id : 'a document -> id -> unit

Assign the state_id of the tip.

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval find_map : 'a document -> (bool -> id option -> 'a -> 'b option) -> 'b
Sourceval 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.

Sourceval unfocus : 'a document -> unit

Undoes a focus.

Sourceval focused : 'a document -> bool

Is the document focused

Sourceval is_empty : 'a document -> bool

No sentences at all

Sourceval before_tip : 'a document -> id * bool

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

Sourceval is_in_focus : 'a document -> id -> bool

Is the id in the focused zone?

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

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

Sourceval 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.

Sourceval print : 'a document -> (bool -> id option -> 'a -> Pp.t) -> Pp.t

debug print

Callbacks on documents

Sourceclass type 'a signals = object ... end
Sourceval connect : 'a document -> 'a signals