package coqide-server
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/coqide-server.core/Document/index.html
Module Document
Source
cut_at d id
cuts the document at id
that is the new tip. Returns the list of sentences that were cut.
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.
look for a sentence validating the predicate. The boolean is true if the sentence is in the zone currently focused.
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
.
returns the 1 to-last sentence, and true if we need to unfocus to reach it.
Folds over the whole document starting from the topmost (maybe unfocused) sentence.
Returns (top,bot) such that the document is morally top @ s @ bot
where s is the focused part.
Callbacks on documents