Xml_parser: detect immediate EOF + disable check_eof by default

 Without this immediate EOF detection, coqtop -ideslave loops
 when its input channel is closed.

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

1 files changed, 17 insertions, 19 deletions

diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 783f5c91b6..81fefd8805 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -42,6 +42,7 @@ type error_msg =
         | AttributeValueExpected
         | EndOfTagExpected of string
         | EOFExpected
+        | Empty
 
 type error = error_msg * error_pos
 
@@ -91,7 +92,7 @@ let make source =
   in
   let () = Xml_lexer.init source in
   {
-    check_eof = true;
+    check_eof = false;
     concat_pcdata = true;
     source = source;
     stack = Stack.create ();
@@ -119,13 +120,13 @@ let rec read_node s =
 	| Xml_lexer.PCData s -> PCData s
 	| Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, [])
 	| Xml_lexer.Tag (tag, attr, false) ->
-          let elements = read_elems ~tag s in
+          let elements = read_elems tag s in
           Element (tag, attr, canonicalize elements)
 	| t ->
 		push t s;
 		raise NoMoreData
 and
-	read_elems ?tag s =
+	read_elems tag s =
 		let elems = ref [] in
 		(try
                   while true do
@@ -139,12 +140,8 @@ and
 		with
 			NoMoreData -> ());
 		match pop s with
-		| Xml_lexer.Endtag s when Some s = tag -> List.rev !elems
-		| Xml_lexer.Eof when tag = None -> List.rev !elems
-		| t ->
-			match tag with
-			| None -> raise (Internal_error EOFExpected)
-			| Some s -> raise (Internal_error (EndOfTagExpected s))
+		| Xml_lexer.Endtag s when s = tag -> List.rev !elems
+		| t -> raise (Internal_error (EndOfTagExpected tag))
 
 let rec read_xml s =
   let node = read_node s in
@@ -164,6 +161,13 @@ let convert = function
 	| Xml_lexer.EAttributeValueExpected -> AttributeValueExpected
 	| Xml_lexer.EUnterminatedEntity -> 	UnterminatedEntity
 
+let error_of_exn xparser = function
+  | NoMoreData when pop xparser = Xml_lexer.Eof -> Empty
+  | NoMoreData -> NodeExpected
+  | Internal_error e -> e
+  | Xml_lexer.Error e -> convert e
+  | e -> raise e
+
 let do_parse xparser =
 	try
 		Xml_lexer.init xparser.source;
@@ -171,16 +175,9 @@ let do_parse xparser =
 		if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
 		Xml_lexer.close ();
 		x
-	with
-		| NoMoreData ->
-			Xml_lexer.close ();
-			raise (!xml_error NodeExpected xparser.source)
-		| Internal_error e ->
-			Xml_lexer.close ();
-			raise (!xml_error e xparser.source)
-		| Xml_lexer.Error e ->
-			Xml_lexer.close ();
-			raise (!xml_error (convert e) xparser.source)
+	with e ->
+	  Xml_lexer.close ();
+	  raise (!xml_error (error_of_exn xparser e) xparser.source)
 
 let parse p = do_parse p
 
@@ -195,6 +192,7 @@ let error_msg = function
         | AttributeValueExpected -> "Attribute value expected"
         | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag
         | EOFExpected -> "End of file expected"
+	| Empty -> "Empty"
 
 let error (msg,pos) =
         if pos.emin = pos.emax then