Robustness fix : clean restart of coqtop on pipe error + force matching

of coqtop return codes.

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

1 files changed, 10 insertions, 3 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index c40343a7e8..fbad08812c 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -104,9 +104,16 @@ object(self)
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
       try
-	Coq.raw_interp coqtop phrase;
-	result#buffer#set_text
-	  ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout coqtop))
+        result#buffer#set_text
+          (match Coq.raw_interp coqtop phrase with
+             | Ide_blob.Fail (l,str) ->
+                 ("Error while interpreting "^phrase^":\n"^str)
+             | Ide_blob.Good () ->
+                 match Coq.read_stdout coqtop with
+                   | Ide_blob.Fail (l,str) ->
+                       ("Error while fetching "^phrase^"results:\n"^str)
+                   | Ide_blob.Good results ->
+                       ("Result for command " ^ phrase ^ ":\n" ^ results))
       with e ->
 	let (s,loc) = Coq.process_exn e in
 	assert (Glib.Utf8.validate s);