Monadification of coqtop queries in CoqIDE

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

1 files changed, 6 insertions, 6 deletions

diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 98ce63faf9..e0a7427798 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -113,14 +113,14 @@ object(self)
       in
       let log level message = result#buffer#insert (message^"\n")
       in
-      let process h k =
-	Coq.interp ~logger:log ~raw:true phrase h (function
-          |Interface.Fail (l,str) ->
+      let process =
+	Coq.bind (Coq.interp ~logger:log ~raw:true phrase) (function
+          | Interface.Fail (l,str) ->
             result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
-	    k ()
-          |Interface.Good res | Interface.Unsafe res ->
+	    Coq.return ()
+          | Interface.Good res | Interface.Unsafe res ->
             result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res);
-	    k ())
+	    Coq.return ())
       in
       result#buffer#set_text "";
       Coq.try_grab coqtop process ignore