From 7ded7df853fd0485822f2a9c79207352af5dca38 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Thu, 16 Jun 2016 13:48:15 +0200
Subject: 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.
---
 ide/ide_slave.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'ide')

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