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, 6 insertions, 6 deletions

diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml
index 048cc6e24a..499d56bd9a 100644
--- a/ide/typed_notebook.ml
+++ b/ide/typed_notebook.ml
@@ -16,14 +16,14 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#append_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Util.list_chop real_pos term_list in
+    let lower,higher = Minilib.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 (* XXX - Temporary hack to compile with archaic lablgtk
   method insert_term ?(build=default_build) ?pos (term:'a) =
     let tab_label,menu_label,page = build term in
     let real_pos = super#insert_page ?tab_label ?menu_label ?pos page in
-    let lower,higher = Util.list_chop real_pos term_list in
+    let lower,higher = Minilib.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
  *)
@@ -32,26 +32,26 @@ object(self)
       (* XXX - Temporary hack to compile with archaic lablgtk *)
     ignore (super#prepend_page ?tab_label ?menu_label page);
     let real_pos = super#page_num page in
-    let lower,higher = Util.list_chop real_pos term_list in
+    let lower,higher = Minilib.list_chop real_pos term_list in
       term_list <- lower@[term]@higher;
       real_pos
 
   method set_term (term:'a) =
     let tab_label,menu_label,page = make_page term in
     let real_pos = super#current_page in
-      term_list <- Util.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
+      term_list <- Minilib.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
       super#set_page ?tab_label ?menu_label page
 
   method get_nth_term i =
     List.nth term_list i
 
   method term_num p =
-    Util.list_index0 p term_list
+    Minilib.list_index0 p term_list
 
   method pages = term_list
 
   method remove_page index =
-    term_list <- Util.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
+    term_list <- Minilib.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
     super#remove_page index
 
   method current_term =