package coqide-server

  1. Overview
  2. Docs
On This Page
  1. Xml Exceptions
The Coq Proof Assistant, XML protocol server

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

doc/coqide-server.protocol/Xml_parser/index.html

Module Xml_parserSource

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

Sourcetype t

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. the Xml.error_msg tells you which error occurred during parsing and the Xml.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 the Xml.parse_file function.
Sourcetype error_pos
Sourcetype error_msg =
  1. | UnterminatedComment
  2. | UnterminatedString
  3. | UnterminatedEntity
  4. | IdentExpected
  5. | CloseExpected
  6. | NodeExpected
  7. | AttributeNameExpected
  8. | AttributeValueExpected
  9. | EndOfTagExpected of string
  10. | EOFExpected
  11. | Empty
Sourcetype error = error_msg * error_pos
Sourceexception Error of error
Sourceexception File_not_found of string
Sourceval error : error -> string

Get a full error message from an Xml error.

Sourceval error_msg : error_msg -> string

Get the Xml error message as a string.

Sourceval line : error_pos -> int

Get the line the error occurred at.

Sourceval range : error_pos -> int * int

Get the relative character range (in current line) the error occurred at.

Sourceval abs_range : error_pos -> int * int

Get the absolute character range the error occurred at.

Sourcetype source =
  1. | SChannel of in_channel
  2. | SString of string
  3. | SLexbuf of Lexing.lexbuf

Several kind of resources can contain Xml documents.

Sourceval make : source -> t

This function returns a new parser with default options.

Sourceval check_eof : t -> bool -> unit

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).

Sourceval parse : ?canonicalize:bool -> t -> xml

Once the parser is configured, you can run the parser on a any kind of xml document source to parse its contents into an Xml data structure.

When canonicalize is set, the parser tries to remove blank PCDATA elements.