STM: better error messages in case of marshal failure

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16829 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 12 deletions

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index dadfc566bc..a15b31da47 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -723,31 +723,35 @@ end = struct (* {{{ *)
 
   open Interface
 
-  exception MarshalError
+  exception MarshalError of string
+
+  let marshal_to_channel oc data =
+    Marshal.to_channel oc data [];
+    flush oc
 
   let marshal_request oc (req : request) =
-    try Marshal.to_channel oc req []; flush oc
-    with Invalid_argument _ -> raise MarshalError
+    try marshal_to_channel oc req
+    with Invalid_argument s -> raise (MarshalError ("marshal_request: "^s))
 
   let unmarshal_request ic =
     try (Marshal.from_channel ic : request)
-    with Invalid_argument _ -> raise MarshalError
+    with Invalid_argument s -> raise (MarshalError ("unmarshal_request: "^s))
 
   let marshal_response oc (res : response) =
-    try Marshal.to_channel oc res []; flush oc
-    with Invalid_argument _ -> raise MarshalError
+    try marshal_to_channel oc res
+    with Invalid_argument s -> raise (MarshalError ("marshal_response: "^s))
   
   let unmarshal_response ic =
     try (Marshal.from_channel ic : response)
-    with Invalid_argument _ -> raise MarshalError
+    with Invalid_argument s -> raise (MarshalError ("unmarshal_response: "^s))
   
   let marshal_more_data oc (res : more_data) =
-    try Marshal.to_channel oc res []; flush oc
-    with Invalid_argument _ -> raise MarshalError
+    try marshal_to_channel oc res
+    with Invalid_argument s -> raise (MarshalError ("marshal_more_data: "^s))
   
   let unmarshal_more_data ic =
     try (Marshal.from_channel ic : more_data)
-    with Invalid_argument _ -> raise MarshalError
+    with Invalid_argument s -> raise (MarshalError ("unmarshal_more_data: "^s))
 
   let queue : task TQueue.t = TQueue.create ()
 
@@ -806,8 +810,8 @@ end = struct (* {{{ *)
         | VCS.Expired -> (* task cancelled: e.g. the user did backtrack *)
             Pp.feedback (Interface.InProgress ~-1);
             prerr_endline ("Task expired: " ^ pr_task task)
-        | MarshalError ->
-            msg_warning(strbrk("Marshalling error. "^
+        | MarshalError s ->
+            msg_warning(strbrk("Marshalling error: "^s^". "^
               "The system state could not be sent to the slave process. "^
               "Falling back to local, lazy, evaluation."));
             let TaskBuildProof (exn_info, _, stop, assign) = task in
@@ -871,6 +875,9 @@ end = struct (* {{{ *)
         let response = slave_respond request in
         marshal_response !slave_oc response;
       with
+      | MarshalError s ->
+        msg_error(str"Slave: "++str s);
+        exit 1
       | e when Errors.noncritical e ->
         (* This can happen if the proof is broken.  The error has also been
          * signalled as a feedback, hence we can silently recover *)