From 8a0d8cfd776650ff08235209792bf32ff55960f4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 12 Nov 2012 13:55:31 +0000
Subject: 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
---
 lib/xml_parser.mli | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'lib/xml_parser.mli')

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
-- 
cgit v1.2.3