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/ideproof.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/ideproof.ml')
| -rw-r--r-- | ide/ideproof.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/ideproof.ml b/ide/ideproof.ml index c84887d1aa..701203061f 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -89,7 +89,7 @@ let mode_cesar (proof:GText.view) = function let display mode (view:GText.view) goals = view#buffer#set_text ""; match goals with - | Ide_blob.Message msg -> + | Ide_intf.Message msg -> view#buffer#insert msg - | Ide_blob.Goals g -> + | Ide_intf.Goals g -> mode view g |