diff options
| author | letouzey | 2011-03-23 17:18:57 +0000 |
|---|---|---|
| committer | letouzey | 2011-03-23 17:18:57 +0000 |
| commit | e84e0f9e4eb6263e870deb1e00929170bc0301ea (patch) | |
| tree | 7a792a8f40c5328c0bd385cec13cb4a65a6b8a3d /ide/command_windows.ml | |
| parent | 461798eeecfd2a59159fb9666874d8ea14209624 (diff) | |
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
Diffstat (limited to 'ide/command_windows.ml')
| -rw-r--r-- | ide/command_windows.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |