package coqide-server
The Rocq Prover, XML protocol server
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/coqide-server.protocol/Richpp/index.html
Module Richpp
Source
This module offers semi-structured pretty-printing.
Each annotation of the semi-structured document refers to the substring it annotates.
rich_pp width ppcmds
returns the interpretation of ppcmds
as a semi-structured document that represents (located) annotations of this string. The get_annotations
function is used to convert tags into the desired annotation. width
sets the printing width of the formatter.
Source
val annotations_positions :
'annotation located Xml_datatype.gxml ->
('annotation * (int * int)) list
annotations_positions ssdoc
returns a list associating each annotations with its position in the string from which ssdoc
is built.
Source
val xml_of_rich_pp :
('annotation -> string) ->
('annotation -> (string * string) list) ->
'annotation located Xml_datatype.gxml ->
Xml_datatype.xml
xml_of_rich_pp ssdoc
returns an XML representation of the semi-structured document ssdoc
.
Enriched text
Type of text with style annotations
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page