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, 5 insertions, 3 deletions

diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
index 1cde9dc811..d48e892561 100644
--- a/lib/xml_parser.mli
+++ b/lib/xml_parser.mli
@@ -57,6 +57,7 @@ type error_msg =
         | AttributeValueExpected
         | EndOfTagExpected of string
         | EOFExpected
+	| Empty
 
 type error = error_msg * error_pos
 
@@ -90,10 +91,11 @@ type source =
 (** This function returns a new parser with default options. *)
 val make : source -> t
 
-(** When a Xml document is parsed, the parser will check that the end of the
+(** 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 off this check by setting
- [check_eof] to [false] {i (by default, check_eof is true)}. *)
+ of returning only the A element. You can turn on this check by setting
+ [check_eof] to [true] {i (by default, check_eof is false, unlike
+ in the original Xmllight)}. *)
 val check_eof : t -> bool -> unit
 
 (** Once the parser is configurated, you can run the parser on a any kind