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/Xml_parser/index.html
Module Xml_parser
Source
Xml Light Parser
While basic parsing functions can be used in the Xml
module, this module is providing a way to create, configure and run an Xml parser.
An Xml node is either Element (tag-name, attributes, children)
or PCData text
Abstract type for an Xml parser.
Xml Exceptions
Several exceptions can be raised when parsing an Xml document :
Xml.Error
is raised when an xml parsing error occurs. theXml.error_msg
tells you which error occurred during parsing and theXml.error_pos
can be used to retrieve the document location where the error occurred at.Xml.File_not_found
is raised when an error occurred while opening a file with theXml.parse_file
function.
Get the relative character range (in current line) the error occurred at.
Several kind of resources can contain Xml documents.
When a Xml document is parsed, the parser may check that the end of the document is reached, so for example parsing "<A/><B/>"
will fail instead of returning only the A element. You can turn on this check by setting check_eof
to true
(by default, check_eof is false, unlike in the original Xmllight).
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page