Ide: more reorganisation and cleanup

 - Avoid using Util which depends on Compat and hence Camlp4
 - Instead, a small Minilib module specific to coqide, which
   duplicate 5 functions from Util (50 lines)
 - some dead code removal
 - the coqlib variable is asked to coqtop
 - remove obsolete Util.check_for_interrupt

 This way, coqide only depends on 3 files outside ide/ :
 Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted
 accordingly.

TODO: how should we signal coqide error, warnings, etc ?
 For the moment, some Printf.eprintf, some failwith.
 To uniformize later...

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

1 files changed, 12 insertions, 16 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 96048c3b30..b1bb1f1831 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,9 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
-open Compat
-open Pp
 open Ideutils
 
 type coqtop = {
@@ -21,18 +18,6 @@ type coqtop = {
 
 let prerr_endline s = if !debug then prerr_endline s else ()
 
-let output = ref (Format.formatter_of_out_channel stdout)
-
-let msg m =
-  let b =  Buffer.create 103 in
-  Pp.msg_with (Format.formatter_of_buffer b) m;
-  Buffer.contents b
-
-let msgnl m =
-  (msg m)^"\n"
-
-let i = ref 0
-
 let get_version_date () =
   let date =
     if Glib.Utf8.validate Coq_config.date
@@ -77,7 +62,8 @@ let coqtop_path () =
 
 let filter_coq_opts args =
   let argstr = String.concat " " (List.map Filename.quote args) in
-  let oc,ic,ec = Unix.open_process_full (coqtop_path () ^" -nois -filteropts "^argstr) (Unix.environment ()) in
+  let cmd = coqtop_path () ^" -nois -filteropts " ^ argstr in
+  let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
   let filtered_args = read_all_lines oc in
   let message = read_all_lines ec in
   match Unix.close_process_full (oc,ic,ec) with
@@ -102,6 +88,16 @@ let check_connection args =
       List.iter Pervasives.prerr_endline lines;
       exit 1
 
+(* TODO: we can probably merge check_connection () and coqlib () *)
+
+let coqlib () =
+  try
+    let ic = Unix.open_process_in (coqtop_path () ^" -where") in
+    let str = input_line ic in
+    ignore (Unix.close_process_in ic);
+    str
+  with _ -> failwith "Error while reading coqlib from coqtop"
+
 let eval_call coqtop (c:'a Ide_intf.call) =
   Marshal.to_channel coqtop.cin c [];
   flush coqtop.cin;