diff options
| -rw-r--r-- | lib/xml_parser.ml | 36 | ||||
| -rw-r--r-- | lib/xml_parser.mli | 8 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 2 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 4 |
4 files changed, 26 insertions, 24 deletions
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml index 783f5c91b..81fefd880 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 diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli index 1cde9dc81..d48e89256 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 diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 5fafe2991..8580bec01 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -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; diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 93ef6596c..473b532dc 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -367,7 +367,6 @@ 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 @@ -375,6 +374,9 @@ let loop () = 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 |