package coqide-server
The Coq Proof Assistant, XML protocol server
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
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