From e84e0f9e4eb6263e870deb1e00929170bc0301ea Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Mar 2011 17:18:57 +0000
Subject: Ide: stronger separation from coqtop

 Former module Ide_blob is now divided in Ide_intf (linked both
 by coqtop and coqide) and Ide_slave (now only in coqtop).
 Ide_intf has almost no dependencies, we can now compile coqide
 with only coq_config.cm* and lib.cm(x)a

 TODO:
  - Devise a better way to display whether coqide is byte or opt
    in the about message (instead of Mltop.is_native, I display
    now the executable name, which hopefully contains opt or byte)
  - Check the late error handling in ide/coq.ml

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

(limited to 'ide/command_windows.ml')

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index a351107d91..70bc4d1cd1 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -106,13 +106,13 @@ object(self)
       try
         result#buffer#set_text
           (match Coq.raw_interp coqtop phrase with
-             | Ide_blob.Fail (l,str) ->
+             | Ide_intf.Fail (l,str) ->
                  ("Error while interpreting "^phrase^":\n"^str)
-             | Ide_blob.Good () ->
+             | Ide_intf.Good () ->
                  match Coq.read_stdout coqtop with
-                   | Ide_blob.Fail (l,str) ->
+                   | Ide_intf.Fail (l,str) ->
                        ("Error while fetching "^phrase^"results:\n"^str)
-                   | Ide_blob.Good results ->
+                   | Ide_intf.Good results ->
                        ("Result for command " ^ phrase ^ ":\n" ^ results))
       with e ->
 	let (s,loc) = Coq.process_exn e in
-- 
cgit v1.2.3