Cleaning up XML parsing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14729 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 12 insertions, 12 deletions

diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 0463c6e30..bf931d75b 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -144,7 +144,13 @@ and
 			| None -> raise (Internal_error EOFExpected)
 			| Some s -> raise (Internal_error (EndOfTagExpected s))
 
-let read_xml s = read_node s
+let rec read_xml s =
+  let node = read_node s in
+  match node with
+  | Element _ -> node
+  | PCData c ->
+    if is_blank c then read_xml s
+    else raise (Xml_lexer.Error Xml_lexer.ENodeExpected)
 
 let convert = function
 	| Xml_lexer.EUnterminatedComment -> UnterminatedComment
@@ -225,3 +231,8 @@ let pos source =
                 emin = min;
                 emax = max;
         }
+
+let () = _raises (fun x p -> 
+        (* local cast : Xml.error_msg -> error_msg *)
+        Error (x, pos p))
+        (fun f -> File_not_found f)
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
index 7f501986b..a3e8aa4ac 100644
--- a/lib/xml_parser.mli
+++ b/lib/xml_parser.mli
@@ -102,8 +102,3 @@ 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
-
-(**/**)
-
-(* internal usage only... *)
-val _raises : (error_msg -> Lexing.lexbuf -> exn) -> (string -> exn) -> unit
diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml
index 2fc1b9065..310035862 100644
--- a/lib/xml_utils.ml
+++ b/lib/xml_utils.ml
@@ -221,9 +221,3 @@ let to_string_fmt x =
 	let s = Buffer.contents tmp in
 	Buffer.reset tmp;
 	s
-
-;;
-Xml_parser._raises (fun x p -> 
-	(* local cast : Xml.error_msg -> error_msg *)
-	Error (x, pos p))
-	(fun f -> File_not_found f);;