From 8e87953db0d1d0a96ed1517e38a25d08092ffad3 Mon Sep 17 00:00:00 2001
From: vgross
Date: Mon, 31 May 2010 22:22:12 +0000
Subject: More indirection.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13042 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq.ml | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

(limited to 'ide')

diff --git a/ide/coq.ml b/ide/coq.ml
index 2db5d81b9c..f385ae0489 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -83,17 +83,22 @@ let version () =
     (if Mltop.is_native then "native" else "bytecode")
     (if Coq_config.best="opt" then "native" else "bytecode")
 
-let is_in_loadpath coqtop s = Ide_blob.eval_call (Ide_blob.is_in_loadpath s)
+let eval_call c =
+  match Ide_blob.eval_call c with
+    | Ide_blob.Good v -> v
+    | Ide_blob.Fail e -> raise e
+
+let is_in_loadpath coqtop s = eval_call (Ide_blob.is_in_loadpath s)
  
 let reset_initial = Ide_blob.reinit
 
-let raw_interp coqtop s = Ide_blob.eval_call (Ide_blob.raw_interp s)
+let raw_interp coqtop s = eval_call (Ide_blob.raw_interp s)
 
-let interp coqtop b s = Ide_blob.eval_call (Ide_blob.interp b s)
+let interp coqtop b s = eval_call (Ide_blob.interp b s)
 
-let rewind coqtop i = Ide_blob.eval_call (Ide_blob.rewind i)
+let rewind coqtop i = eval_call (Ide_blob.rewind i)
  
-let read_stdout coqtop = Ide_blob.eval_call Ide_blob.read_stdout
+let read_stdout coqtop = eval_call Ide_blob.read_stdout
 
 module PrintOpt =
 struct
@@ -160,8 +165,8 @@ type  tried_tactic =
 
 let goals coqtop =
   PrintOpt.enforce_hack ();
-  Ide_blob.eval_call Ide_blob.current_goals
+  eval_call Ide_blob.current_goals
 
-let make_cases coqtop s = Ide_blob.eval_call (Ide_blob.make_cases s)
+let make_cases coqtop s = eval_call (Ide_blob.make_cases s)
 
-let current_status coqtop = Ide_blob.eval_call Ide_blob.current_status
+let current_status coqtop = eval_call Ide_blob.current_status
-- 
cgit v1.2.3