From 1f26b8591f3698699ee2143f5244a5d57243e283 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 24 Nov 2011 13:09:24 +0000
Subject: Moving XML handling to lib directory

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14723 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/xml_parser.mli | 115 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 115 insertions(+)
 create mode 100644 lib/xml_parser.mli

(limited to 'lib/xml_parser.mli')

diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
new file mode 100644
index 0000000000..34dec792d9
--- /dev/null
+++ b/lib/xml_parser.mli
@@ -0,0 +1,115 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+ *)
+
+(** 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] *)
+type xml = 
+        | Element of (string * (string * string) list * xml list)
+        | PCData of string
+
+(** Abstract type for an Xml parser. *)
+type t
+
+(** {6:exc Xml Exceptions} *)
+
+(** Several exceptions can be raised when parsing an Xml document : {ul
+        {li {!Xml.Error} is raised when an xml parsing error occurs. the
+                {!Xml.error_msg} tells you which error occured during parsing
+                and the {!Xml.error_pos} can be used to retreive the document
+                location where the error occured at.}
+        {li {!Xml.File_not_found} is raised when and error occured while
+                opening a file with the {!Xml.parse_file} function.
+        }
+ *)
+
+type error_pos
+
+type error_msg =
+        | UnterminatedComment
+        | UnterminatedString
+        | UnterminatedEntity
+        | IdentExpected
+        | CloseExpected
+        | NodeExpected
+        | AttributeNameExpected
+        | AttributeValueExpected
+        | EndOfTagExpected of string
+        | EOFExpected
+
+type error = error_msg * error_pos
+
+exception Error of error
+
+exception File_not_found of string
+
+(** Get a full error message from an Xml error. *)
+val error : error -> string
+
+(** Get the Xml error message as a string. *)
+val error_msg : error_msg -> string 
+
+(** Get the line the error occured at. *)
+val line : error_pos -> int
+
+(** Get the relative character range (in current line) the error occured at.*)
+val range : error_pos -> int * int
+
+(** Get the absolute character range the error occured at. *)
+val abs_range : error_pos -> int * int
+
+val pos : Lexing.lexbuf -> error_pos
+
+(** Several kind of resources can contain Xml documents. *)
+type source = 
+	| SFile of string
+	| SChannel of in_channel
+	| SString of string
+	| SLexbuf of Lexing.lexbuf
+
+(** This function returns a new parser with default options. *)
+val make : unit -> t
+
+(** When a Xml document is parsed, the parser will 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 off this check by setting
+ [check_eof] to [false] {i (by default, check_eof is true)}. *)
+val check_eof : t -> bool -> unit
+
+(** Once the parser is configurated, you can run the parser on a any kind
+ of xml document source to parse its contents into an Xml data structure. *)
+val parse :  t -> source -> xml
+
+(** When several PCData elements are separed by a \n (or \r\n), you can
+ either split the PCData in two distincts PCData or merge them with \n
+ as seperator into one PCData. The default behavior is to concat the
+ PCData, but this can be changed for a given parser with this flag. *)
+val concat_pcdata : t -> bool -> unit
+
+(**/**)
+
+(* internal usage only... *)
+val _raises : (error_msg -> Lexing.lexbuf -> exn) -> (string -> exn) -> unit
-- 
cgit v1.2.3