diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 13:48:15 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 14:23:56 +0200 |
| commit | 7ded7df853fd0485822f2a9c79207352af5dca38 (patch) | |
| tree | 09fd579374bab505782d809d16767dd7d43653df /ide | |
| parent | f9a619753644ba8e0f0ca1218396c8efee52b544 (diff) | |
ideslave: do not bail out in case of XML error
Used to be an `exit 1`, now an error message is printed on stderr.
This helps people experimenting with the XML protocol.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 79affb36f..9f10b2502 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -1,4 +1,5 @@ (************************************************************************) + (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) @@ -47,6 +48,7 @@ let init_stdout, read_stdout = let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s +let pr_error s = pr_with_pid s let pr_debug s = if !Flags.debug then pr_with_pid s let pr_debug_call q = @@ -517,11 +519,11 @@ let loop () = pr_debug "End of input, exiting gracefully."; exit 0 | Xml_parser.Error (err, loc) -> - pr_debug ("Syntax error in query: " ^ Xml_parser.error_msg err); - exit 1 - | Serialize.Marshal_error _ -> - pr_debug "Incorrect query."; - exit 1 + pr_error ("XML syntax error: " ^ Xml_parser.error_msg err) + | Serialize.Marshal_error (msg,node) -> + pr_error "Unexpected XML message"; + pr_error ("Expected XML node: " ^ msg); + pr_error ("XML tree received: " ^ Xml_printer.to_string_fmt node) | any -> pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any); exit 1 |