package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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.

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.

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

Assign the state_id of the tip.

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct