Permalink
Browse files

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
  • Loading branch information...
1 parent d7f0d75 commit 8a0d8cfd776650ff08235209792bf32ff55960f4 letouzey committed Nov 12, 2012
Showing with 26 additions and 24 deletions.
  1. +17 −19 lib/xml_parser.ml
  2. +5 −3 lib/xml_parser.mli
  3. +1 −1 tools/fake_ide.ml
  4. +3 −1 toplevel/ide_slave.ml
View
@@ -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,23 +161,23 @@ 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;
let x = read_xml xparser in
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
View
@@ -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
View
@@ -87,7 +87,7 @@ let main =
let coqtop =
let (cin, cout) = Unix.open_process (coqtop_name^" -ideslave") in
let p = Xml_parser.make (Xml_parser.SChannel cin) in
- let () = Xml_parser.check_eof p false in {
+ {
in_chan = cin;
out_chan = cout;
xml_parser = p;
View
@@ -367,14 +367,16 @@ let loop () =
let xml_answer =
try
let p = Xml_parser.make (Xml_parser.SChannel stdin) in
- let () = Xml_parser.check_eof p false in
let xml_query = Xml_parser.parse p in
let q = Serialize.to_call xml_query in
let () = pr_debug ("<-- " ^ Serialize.pr_call q) in
let r = eval_call q in
let () = pr_debug ("--> " ^ Serialize.pr_full_value q r) in
Serialize.of_answer q r
with
+ | Xml_parser.Error (Xml_parser.Empty, _) ->
+ pr_debug ("End of input, exiting");
+ exit 0
| Xml_parser.Error (err, loc) ->
let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in
fail msg

0 comments on commit 8a0d8cf

Please sign in to comment.