From a90ccfa5f25858e8cb224b4cfa4f724ca84e3ea4 Mon Sep 17 00:00:00 2001
From: vgross
Date: Mon, 5 Jul 2010 17:21:42 +0000
Subject: 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
---
 ide/command_windows.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'ide/command_windows.ml')

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