Imported Upstream snapshot 8.3~beta0+13298

11 files changed, 147 insertions, 1219 deletions

diff --git a/ide/utils/config_file.ml b/ide/utils/config_file.ml
index d972639f..37f2e9a4 100644
--- a/ide/utils/config_file.ml
+++ b/ide/utils/config_file.ml
@@ -23,7 +23,7 @@
 (*                                                                               *)
 (*********************************************************************************)
 
-(* $Id: config_file.ml 10348 2007-12-06 17:36:14Z aspiwack $ *)
+(* $Id$ *)
 
 (* TODO *)
 (* section comments *)
diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml
index 275d8616..05bf54eb 100644
--- a/ide/utils/configwin.ml
+++ b/ide/utils/configwin.ml
@@ -43,9 +43,7 @@ class key_cp = Configwin_types.key_cp
 
 
 let string = Configwin_ihm.string
-let custom_string = Configwin_ihm.custom_string
 let text = Configwin_ihm.text
-let custom_text = Configwin_ihm.custom_text
 let strings = Configwin_ihm.strings
 let list = Configwin_ihm.list
 let bool = Configwin_ihm.bool
diff --git a/ide/utils/configwin.mli b/ide/utils/configwin.mli
index 2d4dd4a7..bbfb7a04 100644
--- a/ide/utils/configwin.mli
+++ b/ide/utils/configwin.mli
@@ -77,13 +77,6 @@ class key_cp :
 val string : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (string -> unit) -> string -> string -> parameter_kind
 
-(** Same as {!Configwin.string} but for values which are not strings. *)
-val custom_string : ?editable: bool -> ?expand: bool -> ?help: string ->
-  ?f: ('a -> unit) ->
-    to_string: ('a -> string) ->
-      of_string: (string -> 'a) ->
-	string -> 'a -> parameter_kind
-
 (** [bool label value] creates a boolean parameter.
    @param editable indicate if the value is editable (default is [true]).
    @param help an optional help message.
@@ -185,13 +178,6 @@ val combo : ?editable: bool -> ?expand: bool -> ?help: string ->
 val text : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (string -> unit) -> string -> string -> parameter_kind
 
-(** Same as {!Configwin.text} but for values which are not strings. *)
-val custom_text : ?editable: bool -> ?expand: bool -> ?help: string ->
-  ?f: ('a -> unit) ->
-    to_string: ('a -> string) ->
-      of_string: (string -> 'a) ->
-	string -> 'a -> parameter_kind
-
 (** Same as {!Configwin.text} but html bindings are available
    in the text widget. Use the [configwin_html_config] utility
    to edit your bindings.
@@ -248,7 +234,7 @@ val hotkey : ?editable: bool -> ?expand: bool -> ?help: string ->
 
 val modifiers : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?allow:(Gdk.Tags.modifier list) ->
-  ?f: (Gdk.Tags.modifier list -> unit) -> 
+  ?f: (Gdk.Tags.modifier list -> unit) ->
     string -> Gdk.Tags.modifier list -> parameter_kind
 
 (** [custom box f expand] creates a custom parameter, with
diff --git a/ide/utils/configwin_html_config.ml b/ide/utils/configwin_html_config.ml
deleted file mode 100644
index fe39de0a..00000000
--- a/ide/utils/configwin_html_config.ml
+++ /dev/null
@@ -1,84 +0,0 @@
-(*********************************************************************************)
-(*                Cameleon                                                       *)
-(*                                                                               *)
-(*    Copyright (C) 2005 Institut National de Recherche en Informatique et       *)
-(*    en Automatique. All rights reserved.                                       *)
-(*                                                                               *)
-(*    This program is free software; you can redistribute it and/or modify       *)
-(*    it under the terms of the GNU Library General Public License as            *)
-(*    published by the Free Software Foundation; either version 2 of the         *)
-(*    License, or  any later version.                                            *)
-(*                                                                               *)
-(*    This program is distributed in the hope that it will be useful,            *)
-(*    but WITHOUT ANY WARRANTY; without even the implied warranty of             *)
-(*    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              *)
-(*    GNU Library General Public License for more details.                       *)
-(*                                                                               *)
-(*    You should have received a copy of the GNU Library General Public          *)
-(*    License along with this program; if not, write to the Free Software        *)
-(*    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA                   *)
-(*    02111-1307  USA                                                            *)
-(*                                                                               *)
-(*    Contact: Maxence.Guesdon@inria.fr                                          *)
-(*                                                                               *)
-(*********************************************************************************)
-
-(** The HTML editor bindings configurator. *)
-
-module C = Configwin_ihm
-open Configwin_types
-open Config_file
-
-let simple_get = C.simple_edit
-    ~with_apply: false ~apply: (fun () -> ())
-
-let params_hb hb =
-  let p_key = C.hotkey
-      ~f: (fun k -> hb.html_key <- k) Configwin_messages.mKey
-      hb.html_key
-  in
-  let p_begin = C.string
-      ~f: (fun s -> hb.html_begin <- s)
-      Configwin_messages.html_begin
-      hb.html_begin
-  in
-  let p_end = C.string
-      ~f: (fun s -> hb.html_end <- s)
-      Configwin_messages.html_end
-      hb.html_end
-  in
-  [ p_key ; p_begin ; p_end ]
-
-let edit_hb hb =
-  ignore (simple_get Configwin_messages.mEdit (params_hb hb));
-  hb
-
-let add () =
-  let hb = { html_key = Configwin_types.string_to_key "C-a" ;
-	     html_begin = "" ;
-	     html_end = "" ;
-	   }
-  in
-  match simple_get Configwin_messages.mAdd (params_hb hb) with
-    Return_ok -> [hb]
-  | _ -> []
-
-let main () =
-  ignore (GMain.Main.init ());
-  let (ini, bindings) = C.html_config_file_and_option () in
-  let param = C.list
-      ~f: (fun l -> bindings#set l ; ini#write Configwin_ihm.file_html_config )
-      ~eq: (fun hb1 hb2 -> hb1.html_key = hb2.html_key)
-      ~edit: edit_hb
-      ~add: add
-      ~titles: [ Configwin_messages.mKey ; Configwin_messages.html_begin ;
-		 Configwin_messages.html_end ]
-      Configwin_messages.shortcuts
-      (fun hb -> [ Configwin_types.key_to_string hb.html_key ;
-		   hb.html_begin ; hb.html_end ])
-      bindings#get
-  in
-  ignore (simple_get ~width: 300 ~height: 400
-	    Configwin_messages.html_config [param])
-
-let _ = main ()
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 3ab3823d..3833acfa 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -802,41 +802,27 @@ class hotkey_param_box param (tt:GData.tooltips) =
 
 class modifiers_param_box param =
   let hbox = GPack.hbox () in
-  let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
+  let wev = GBin.event_box ~packing: (hbox#pack ~expand:true ~fill:true ~padding: 2) () in
   let _wl = GMisc.label ~text: param.md_label ~packing: wev#add () in
-  let we = GEdit.entry
-      ~editable: false
-      ~packing: (hbox#pack ~expand: param.md_expand ~padding: 2)
-      ()
-  in
   let value = ref param.md_value in
-  let _ = 
+  let _ = List.map (fun modifier ->
+                      let but = GButton.toggle_button
+                                  ~label:(Configwin_types.modifiers_to_string [modifier])
+                                  ~active:(List.mem modifier param.md_value)
+                                  ~packing:(hbox#pack ~expand:false) () in
+                      ignore (but#connect#toggled
+                                (fun _ -> if but#active then value := modifier::!value
+                                 else value := List.filter ((<>) modifier) !value)))
+            param.md_allow
+  in
+  let _ =
     match param.md_help with
       None -> ()
     | Some help ->
-	let tooltips = GData.tooltips () in
-	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
-	tooltips#set_tip wev#coerce ~text: help ~privat: help 
-  in
-  let _ = we#set_text (Configwin_types.modifiers_to_string param.md_value) in
-  let mods_we_care = param.md_allow in
-  let capture ev =
-    let modifiers = GdkEvent.Key.state ev in
-    let mods = List.filter
-	(fun m -> (List.mem m mods_we_care))
-	modifiers
-    in
-    value := mods;
-    we#set_text (Configwin_types.modifiers_to_string !value);
-    false
-  in
-  let _ = 
-    if param.md_editable then
-      ignore (we#event#connect#key_press capture)
-    else
-      ()
+       let tooltips = GData.tooltips () in
+       ignore (hbox#connect#destroy ~callback: tooltips#destroy);
+       tooltips#set_tip wev#coerce ~text: help ~privat: help
   in
-
   object (self)
     (** This method returns the main box ready to be packed. *)
     method box = hbox#coerce
@@ -1093,13 +1079,13 @@ let edit ?(with_apply=true)
       (fun conf_struct -> new configuration_box tooltips conf_struct wnote)
       conf_struct_list
   in
-    
+
     if with_apply then
       dialog#add_button Configwin_messages.mApply `APPLY;
-    
+
     dialog#add_button Configwin_messages.mOk `OK;
     dialog#add_button Configwin_messages.mCancel `CANCEL;
-    
+
     let f_apply () =
       List.iter (fun param_box -> param_box#apply) list_param_box  ;
       apply ()
@@ -1245,22 +1231,6 @@ let string ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       string_of_string = (fun x -> x) ;
     }
 
-(** Create a custom string param. *)
-let custom_string ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) ~to_string ~of_string label v =
-  String_param
-    (Configwin_types.mk_custom_text_string_param
-       {
-	 string_label = label ;
-	 string_help = help ;
-	 string_value = v ;
-	 string_editable = editable ;
-	 string_f_apply = f ;
-	 string_expand = expand ;
-	 string_to_string = to_string;
-	 string_of_string = of_string ;
-       }
-    )
-
 (** Create a bool param. *)
 let bool ?(editable=true) ?help ?(f=(fun _ -> ())) label v =
   Bool_param
@@ -1282,23 +1252,21 @@ let list ?(editable=true) ?help
     label (f_strings : 'a -> string list) v =
   List_param
     (fun tt ->
-      Obj.magic
-	(new list_param_box
-	   {
-	     list_label = label ;
-	     list_help = help ;
-	     list_value = v ;
-	     list_editable = editable ;
-	     list_titles = titles;
-	     list_eq = eq ;
-	     list_strings = f_strings ;
-	     list_color = color ;
-	     list_f_edit = edit ;
-	     list_f_add = add ;
-	     list_f_apply = f ;
-	   }
-	   tt
-	)
+	new list_param_box
+	  {
+	    list_label = label ;
+	    list_help = help ;
+	    list_value = v ;
+	    list_editable = editable ;
+	    list_titles = titles;
+	    list_eq = eq ;
+	    list_strings = f_strings ;
+	    list_color = color ;
+	    list_f_edit = edit ;
+	    list_f_add = add ;
+	    list_f_apply = f ;
+	  }
+	  tt
     )
 
 (** Create a strings param. *)
@@ -1363,22 +1331,6 @@ let text ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       string_of_string = (fun x -> x) ;
     }
 
-(** Create a custom text param. *)
-let custom_text ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) ~to_string ~of_string label v =
-  Text_param
-    (Configwin_types.mk_custom_text_string_param
-       {
-	 string_label = label ;
-	 string_help = help ;
-	 string_value = v ;
-	 string_editable = editable ;
-	 string_f_apply = f ;
-	 string_expand = expand ;
-	 string_to_string = to_string;
-	 string_of_string = of_string ;
-       }
-    )
-
 (** Create a html param. *)
 let html ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
   Html_param
@@ -1441,11 +1393,11 @@ let hotkey ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       hk_expand = expand ;
     }
 
-let modifiers 
-  ?(editable=true) 
-  ?(expand=true) 
-  ?help 
-  ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5]) 
+let modifiers
+  ?(editable=true)
+  ?(expand=true)
+  ?help
+  ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5])
   ?(f=(fun _ -> ())) label v =
   Modifiers_param
     {
@@ -1456,7 +1408,7 @@ let modifiers
       md_f_apply = f ;
       md_expand = expand ;
       md_allow = allow ;
-    } 
+    }
 
 (** Create a custom param.*)
 let custom ?label box f expand =
diff --git a/ide/utils/configwin_keys.ml b/ide/utils/configwin_keys.ml
index e1d7f33b..9f44e5c6 100644
--- a/ide/utils/configwin_keys.ml
+++ b/ide/utils/configwin_keys.ml
@@ -25,7 +25,7 @@
 
 (** Key codes
 
-   Ce fichier provient de X11/keysymdef.h 
+   Ce fichier provient de X11/keysymdef.h
    les noms des symboles deviennent : XK_ -> xk_
 
    Thanks to Fabrice Le Fessant.
@@ -1334,11 +1334,11 @@ let xk_Thai_khokhai					= 0xda2
 let xk_Thai_khokhuat				= 0xda3
 let xk_Thai_khokhwai				= 0xda4
 let xk_Thai_khokhon					= 0xda5
-let xk_Thai_khorakhang			        = 0xda6  
-let xk_Thai_ngongu					= 0xda7  
-let xk_Thai_chochan					= 0xda8  
-let xk_Thai_choching				= 0xda9   
-let xk_Thai_chochang				= 0xdaa  
+let xk_Thai_khorakhang			        = 0xda6
+let xk_Thai_ngongu					= 0xda7
+let xk_Thai_chochan					= 0xda8
+let xk_Thai_choching				= 0xda9
+let xk_Thai_chochang				= 0xdaa
 let xk_Thai_soso					= 0xdab
 let xk_Thai_chochoe					= 0xdac
 let xk_Thai_yoying					= 0xdad
@@ -1380,39 +1380,39 @@ let xk_Thai_saraa					= 0xdd0
 let xk_Thai_maihanakat				= 0xdd1
 let xk_Thai_saraaa					= 0xdd2
 let xk_Thai_saraam					= 0xdd3
-let xk_Thai_sarai					= 0xdd4   
-let xk_Thai_saraii					= 0xdd5   
-let xk_Thai_saraue					= 0xdd6    
-let xk_Thai_sarauee					= 0xdd7    
-let xk_Thai_sarau					= 0xdd8    
-let xk_Thai_sarauu					= 0xdd9   
+let xk_Thai_sarai					= 0xdd4
+let xk_Thai_saraii					= 0xdd5
+let xk_Thai_saraue					= 0xdd6
+let xk_Thai_sarauee					= 0xdd7
+let xk_Thai_sarau					= 0xdd8
+let xk_Thai_sarauu					= 0xdd9
 let xk_Thai_phinthu					= 0xdda
 let xk_Thai_maihanakat_maitho   			= 0xdde
 let xk_Thai_baht					= 0xddf
-let xk_Thai_sarae					= 0xde0    
+let xk_Thai_sarae					= 0xde0
 let xk_Thai_saraae					= 0xde1
 let xk_Thai_sarao					= 0xde2
-let xk_Thai_saraaimaimuan				= 0xde3   
-let xk_Thai_saraaimaimalai				= 0xde4  
+let xk_Thai_saraaimaimuan				= 0xde3
+let xk_Thai_saraaimaimalai				= 0xde4
 let xk_Thai_lakkhangyao				= 0xde5
 let xk_Thai_maiyamok				= 0xde6
 let xk_Thai_maitaikhu				= 0xde7
-let xk_Thai_maiek					= 0xde8   
+let xk_Thai_maiek					= 0xde8
 let xk_Thai_maitho					= 0xde9
 let xk_Thai_maitri					= 0xdea
 let xk_Thai_maichattawa				= 0xdeb
 let xk_Thai_thanthakhat				= 0xdec
 let xk_Thai_nikhahit				= 0xded
-let xk_Thai_leksun					= 0xdf0 
-let xk_Thai_leknung					= 0xdf1  
-let xk_Thai_leksong					= 0xdf2 
+let xk_Thai_leksun					= 0xdf0
+let xk_Thai_leknung					= 0xdf1
+let xk_Thai_leksong					= 0xdf2
 let xk_Thai_leksam					= 0xdf3
-let xk_Thai_leksi					= 0xdf4  
-let xk_Thai_lekha					= 0xdf5  
-let xk_Thai_lekhok					= 0xdf6  
-let xk_Thai_lekchet					= 0xdf7  
-let xk_Thai_lekpaet					= 0xdf8  
-let xk_Thai_lekkao					= 0xdf9 
+let xk_Thai_leksi					= 0xdf4
+let xk_Thai_lekha					= 0xdf5
+let xk_Thai_lekhok					= 0xdf6
+let xk_Thai_lekchet					= 0xdf7
+let xk_Thai_lekpaet					= 0xdf8
+let xk_Thai_lekkao					= 0xdf9
 
 
 (*
diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml
index 0def0b25..90d5756b 100644
--- a/ide/utils/configwin_types.ml
+++ b/ide/utils/configwin_types.ml
@@ -111,7 +111,7 @@ let modifiers_to_string m =
                   ) ^ s)
   in
     iter m ""
-      
+
 let value_to_key v =
   match v with
     Raw.String s -> string_to_key s
@@ -233,7 +233,7 @@ type hotkey_param = {
 
 type modifiers_param = {
     md_label : string ; (** the label of the parameter *)
-    mutable md_value : Gdk.Tags.modifier list ; 
+    mutable md_value : Gdk.Tags.modifier list ;
              (** The value, as a list of modifiers and a key code *)
     md_editable : bool ; (** indicates if the value can be changed *)
     md_f_apply : Gdk.Tags.modifier list -> unit ;
@@ -241,11 +241,7 @@ type modifiers_param = {
     md_help : string option ; (** optional help string *)
     md_expand : bool ; (** expand or not *)
     md_allow : Gdk.Tags.modifier list
-  } 
-
-
-let mk_custom_text_string_param (a : 'a string_param) : string string_param =
-  Obj.magic a
+  }
 
 
 (** This type represents the different kinds of parameters. *)
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
index 5441f4ab..1ab107c7 100644
--- a/ide/utils/editable_cells.ml
+++ b/ide/utils/editable_cells.ml
@@ -1,21 +1,21 @@
 open GTree
 open Gobject
 
-let create l = 
+let create l =
   let hbox = GPack.hbox () in
-  let scw = GBin.scrolled_window 
-	      ~hpolicy:`AUTOMATIC 
-	      ~vpolicy:`AUTOMATIC 
+  let scw = GBin.scrolled_window
+	      ~hpolicy:`AUTOMATIC
+	      ~vpolicy:`AUTOMATIC
 	      ~packing:(hbox#pack ~expand:true) () in
 
   let columns = new GTree.column_list in
   let command_col =  columns#add Data.string in
   let coq_col = columns#add Data.string in
   let store = GTree.list_store columns
-  in 
+  in
 
 (* populate the store *)
-  let _ = List.iter (fun (x,y) -> 
+  let _ = List.iter (fun (x,y) ->
 		       let row = store#append () in
 		       store#set ~row ~column:command_col x;
 		       store#set ~row ~column:coq_col y)
@@ -27,61 +27,61 @@ let create l =
   view#set_rules_hint true;
 
   let renderer_comm = GTree.cell_renderer_text [`EDITABLE true]  in
-  ignore (renderer_comm#connect#edited 
-    ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
-		 store#set 
-		 ~row:(store#get_iter path) 
+  ignore (renderer_comm#connect#edited
+    ~callback:(fun (path:Gtk.tree_path) (s:string) ->
+		 store#set
+		 ~row:(store#get_iter path)
 		 ~column:command_col s));
-  let first = 
-    GTree.view_column ~title:"Coq Command to try" 
-      ~renderer:(renderer_comm,["text",command_col]) 
-      () 
+  let first =
+    GTree.view_column ~title:"Coq Command to try"
+      ~renderer:(renderer_comm,["text",command_col])
+      ()
   in ignore (view#append_column first);
 
   let renderer_coq = GTree.cell_renderer_text [`EDITABLE true] in
   ignore(renderer_coq#connect#edited
-	   ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
-			store#set 
-			~row:(store#get_iter path) 
+	   ~callback:(fun (path:Gtk.tree_path) (s:string) ->
+			store#set
+			~row:(store#get_iter path)
 			~column:coq_col s));
-  let second = 
-    GTree.view_column ~title:"Coq Command to insert" 
-      ~renderer:(renderer_coq,["text",coq_col]) 
-      () 
+  let second =
+    GTree.view_column ~title:"Coq Command to insert"
+      ~renderer:(renderer_coq,["text",coq_col])
+      ()
   in ignore (view#append_column second);
 
-  let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD () 
+  let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD ()
   in
   let up = GButton.button  ~stock:`GO_UP ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in
-  let down = GButton.button 
-	       ~stock:`GO_DOWN 
-	       ~label:"Down" 
-	       ~packing:(vbox#pack ~expand:true ~fill:false) () 
+  let down = GButton.button
+	       ~stock:`GO_DOWN
+	       ~label:"Down"
+	       ~packing:(vbox#pack ~expand:true ~fill:false) ()
   in
-  let add = GButton.button ~stock:`ADD 
-	      ~label:"Add" 
-	      ~packing:(vbox#pack ~expand:true ~fill:false) 
-	      () 
+  let add = GButton.button ~stock:`ADD
+	      ~label:"Add"
+	      ~packing:(vbox#pack ~expand:true ~fill:false)
+	      ()
   in
-  let remove = GButton.button ~stock:`REMOVE 
-		 ~label:"Remove" 
-		 ~packing:(vbox#pack ~expand:true ~fill:false) () 
+  let remove = GButton.button ~stock:`REMOVE
+		 ~label:"Remove"
+		 ~packing:(vbox#pack ~expand:true ~fill:false) ()
   in
 
-  ignore (add#connect#clicked 
-	    ~callback:(fun b ->  
+  ignore (add#connect#clicked
+	    ~callback:(fun b ->
 			 let n = store#append () in
 			 view#selection#select_iter n));
-  ignore (remove#connect#clicked 
-	    ~callback:(fun b -> match view#selection#get_selected_rows with 
+  ignore (remove#connect#clicked
+	    ~callback:(fun b -> match view#selection#get_selected_rows with
 			 | [] -> ()
 			 | path::_ ->
 			     let iter = store#get_iter path in
 		       	     ignore (store#remove iter);
 		      ));
-  ignore (up#connect#clicked 
-	    ~callback:(fun b ->  
-			 match view#selection#get_selected_rows with 
+  ignore (up#connect#clicked
+	    ~callback:(fun b ->
+			 match view#selection#get_selected_rows with
 			   | [] -> ()
 			   | path::_ ->
 			       let iter = store#get_iter path in
@@ -89,9 +89,9 @@ let create l =
 			       let upiter = store#get_iter path in
 			       ignore (store#swap iter upiter);
 		      ));
-  ignore (down#connect#clicked 
-	    ~callback:(fun b ->  
-			 match view#selection#get_selected_rows with 
+  ignore (down#connect#clicked
+	    ~callback:(fun b ->
+			 match view#selection#get_selected_rows with
 			   | [] -> ()
 			   | path::_ ->
 			       let iter = store#get_iter path in
@@ -100,13 +100,13 @@ let create l =
 			       ignore (store#swap iter upiter)
 			       with _ -> ()
 		      ));
-  let get_data () = 
+  let get_data () =
     let start_path = GtkTree.TreePath.from_string "0" in
     let start_iter = store#get_iter start_path in
-    let rec all acc = 
+    let rec all acc =
       let new_acc = (store#get ~row:start_iter ~column:command_col,
 		     store#get ~row:start_iter ~column:coq_col)::acc
-      in      
+      in
       if store#iter_next start_iter then all new_acc else List.rev new_acc
     in all []
   in
diff --git a/ide/utils/okey.mli b/ide/utils/okey.mli
index c8d48389..84ea4df4 100644
--- a/ide/utils/okey.mli
+++ b/ide/utils/okey.mli
@@ -23,7 +23,7 @@
 (*                                                                               *)
 (*********************************************************************************)
 
-(** Okey interface. 
+(** Okey interface.
 
    Once the lib is compiled and installed, you can use it by referencing
    it with the [Okey] module. You must add [okey.cmo] or [okey.cmx]
@@ -35,7 +35,7 @@ type modifier = Gdk.Tags.modifier
 (** Set the default modifier list. The first default value is [[]].*)
 val set_default_modifiers : modifier list -> unit
 
-(** Set the default modifier mask. The first default value is 
+(** Set the default modifier mask. The first default value is
    [[`MOD2 ; `MOD3 ; `MOD4 ; `MOD5 ; `LOCK]].
    The mask defines the modifiers not taken into account
    when looking for the handler of a key press event.
@@ -48,67 +48,67 @@ val set_default_mask : modifier list -> unit
    @param remove when true, the previous handlers for the given key and modifier
    list are not kept.
    @param cond this function is a guard: the [callback] function is not called
-   if the [cond] function returns [false]. 
+   if the [cond] function returns [false].
    The default [cond] function always returns [true].
 
    @param mods the list of modifiers. If not given, the default modifiers
-   are used. 
+   are used.
    You can set the default modifiers with function {!Okey.set_default_modifiers}.
 
    @param mask the list of modifiers which must not be taken
    into account to trigger the given handler. [mods]
    and [mask] must not have common modifiers. If not given, the default mask
-   is used. 
+   is used.
    You can set the default modifiers mask with function {!Okey.set_default_mask}.
 *)
 val add :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
-      event : GObj.event_ops; get_oid : int; .. > -> 
-	?cond: (unit -> bool) -> 
-	  ?mods: modifier list -> 
-	    ?mask: modifier list -> 
-	      Gdk.keysym -> 
-		(unit -> unit) -> 
+      event : GObj.event_ops; get_oid : int; .. > ->
+	?cond: (unit -> bool) ->
+	  ?mods: modifier list ->
+	    ?mask: modifier list ->
+	      Gdk.keysym ->
+		(unit -> unit) ->
 		  unit
 
 (** It calls {!Okey.add} for each given key.*)
-val add_list : 
+val add_list :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
-      event : GObj.event_ops; get_oid : int; .. > -> 
-	?cond: (unit -> bool) -> 
-	  ?mods: modifier list -> 
-	    ?mask: modifier list -> 
-	      Gdk.keysym list -> 
-		(unit -> unit) -> 
+      event : GObj.event_ops; get_oid : int; .. > ->
+	?cond: (unit -> bool) ->
+	  ?mods: modifier list ->
+	    ?mask: modifier list ->
+	      Gdk.keysym list ->
+		(unit -> unit) ->
 		  unit
-	      
+
 (** Like {!Okey.add} but the previous handlers for the
    given modifiers and key are not kept.*)
 val set :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
-      event : GObj.event_ops; get_oid : int; .. > -> 
-	?cond: (unit -> bool) -> 
-	  ?mods: modifier list -> 
-	    ?mask: modifier list -> 
-	      Gdk.keysym -> 
-		(unit -> unit) -> 
+      event : GObj.event_ops; get_oid : int; .. > ->
+	?cond: (unit -> bool) ->
+	  ?mods: modifier list ->
+	    ?mask: modifier list ->
+	      Gdk.keysym ->
+		(unit -> unit) ->
 		  unit
 
 (** It calls {!Okey.set} for each given key.*)
-val set_list : 
+val set_list :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
       event : GObj.event_ops; get_oid : int; .. > ->
-	?cond: (unit -> bool) -> 
-	  ?mods: modifier list -> 
-	    ?mask: modifier list -> 
-	      Gdk.keysym list -> 
-		(unit -> unit) -> 
+	?cond: (unit -> bool) ->
+	  ?mods: modifier list ->
+	    ?mask: modifier list ->
+	      Gdk.keysym list ->
+		(unit -> unit) ->
 		  unit
 
 (** Remove the handlers associated to the given widget.
    This is automatically done when a widget is destroyed but
    you can do it yourself. *)
-val remove_widget : 
+val remove_widget :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
       event : GObj.event_ops; get_oid : int; .. > ->
 	unit ->
diff --git a/ide/utils/uoptions.ml b/ide/utils/uoptions.ml
deleted file mode 100644
index aa3b42cd..00000000
--- a/ide/utils/uoptions.ml
+++ /dev/null
@@ -1,772 +0,0 @@
-(**************************************************************************)
-(*                   Cameleon                                             *)
-(*                                                                        *)
-(*      Copyright (C) 2002 Institut National de Recherche en Informatique et   *)
-(*      en Automatique. All rights reserved.                              *)
-(*                                                                        *)
-(*      This program is free software; you can redistribute it and/or modify  *)
-(*      it under the terms of the GNU General Public License as published by  *)
-(*      the Free Software Foundation; either version 2 of the License, or  *)
-(*      any later version.                                                *)
-(*                                                                        *)
-(*      This program is distributed in the hope that it will be useful,   *)
-(*      but WITHOUT ANY WARRANTY; without even the implied warranty of    *)
-(*      MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     *)
-(*      GNU General Public License for more details.                      *)
-(*                                                                        *)
-(*      You should have received a copy of the GNU General Public License  *)
-(*      along with this program; if not, write to the Free Software       *)
-(*      Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA          *)
-(*      02111-1307  USA                                                   *)
-(*                                                                        *)
-(*      Contact: Maxence.Guesdon@inria.fr                                *)
-(**************************************************************************)
-
-(** Simple options:
-  This will enable very simple configuration, by a mouse-based configurator.
-  Flags.will be defined by a special function, which will also check
-  if a value has been provided  by the user in its .gwmlrc file.
-  The .gwmlrc will be created by a dedicated tool, which could be used
-  to generate both .gwmlrc and .efunsrc files.
-
-Note: this is redundant, since such options could also be better set
-in the .Xdefaults file (using Xrm to load them). Maybe we should merge
-both approaches in a latter release.
-  
-   Code from Fabrice Le Fessant.
-
-    *)
-  
-type option_value =
-    Module of option_module
-  | StringValue of string
-  | IntValue of int
-  | FloatValue of float
-  | List of option_value list
-  | SmallList of option_value list
-and option_module = (string * option_value) list
-;;
-
-
-
-type 'a option_class =
-  { class_name : string;
-    from_value : option_value -> 'a;
-    to_value : 'a -> option_value;
-    mutable class_hooks : ('a option_record -> unit) list }
-  
-and 'a option_record =
-  { option_name : string list;
-    option_class : 'a option_class;
-    mutable option_value : 'a;
-    option_help : string;
-    mutable option_hooks : (unit -> unit) list;
-    mutable string_wrappers : (('a -> string) * (string -> 'a)) option;
-    option_file : options_file;
-  }
-  
-and options_file = {
-    mutable file_name : string; 
-    mutable file_options : Obj.t option_record list;
-    mutable file_rc : option_module;
-    mutable file_pruned : bool;
-  }
-;;
-
-let create_options_file name =
-  ignore
-    (
-     if not (Sys.file_exists name) then
-       let oc = open_out name in 
-       close_out oc
-    );
-  {
-    file_name = name;
-    file_options =[];
-    file_rc = [];
-    file_pruned = false;
-  }
-  
-let set_options_file opfile name = opfile.file_name <- name
-
-let
-  define_option_class
-    (class_name : string)
-    (from_value : option_value -> 'a)
-    (to_value : 'a -> option_value) =
-  let c =
-    {class_name = class_name; 
-      from_value = from_value; 
-      to_value = to_value;
-     class_hooks = []}
-  in
-  c
-;;  
-
-(*
-let filename =
-  ref
-    (Filename.concat Sysenv.home
-       ("." ^ Filename.basename Sys.argv.(0) ^ "rc"))
-;;
-let gwmlrc = ref [];;
-
-let options = ref [];;
-*)
-
-let rec find_value list m =
-  match list with
-    [] -> raise Not_found
-  | name :: tail ->
-      let m = List.assoc name m in
-      match m, tail with
-        _, [] -> m
-      | Module m, _ :: _ -> find_value tail m
-      | _ -> raise Not_found
-;;
-
-let prune_file file =
-  file.file_pruned <- true
-
-let
-  define_option
-    (opfile : options_file)
-    (option_name : string list)
-    (option_help : string)
-    (option_class : 'a option_class)
-    (default_value : 'a) =
-  let o =
-    {option_name = option_name; 
-      option_help = option_help;
-      option_class = option_class; 
-      option_value = default_value;
-      string_wrappers = None;
-      option_hooks = []; 
-      option_file = opfile; }
-  in
-  opfile.file_options <- (Obj.magic o : Obj.t option_record) ::
-    opfile.file_options;
-  o.option_value <-
-    begin try o.option_class.from_value (find_value option_name 
-        opfile.file_rc) with
-      Not_found -> default_value
-    | e ->
-        Printf.printf "Flags.define_option, for option %s: "
-          (match option_name with
-             [] -> "???"
-           | name :: _ -> name);
-        Printf.printf "%s" (Printexc.to_string e);
-        print_newline ();
-        default_value
-    end;
-  o
-;;
-
-  
-open Genlex;;
-  
-let lexer = make_lexer ["="; "{"; "}"; "["; "]"; ";"; "("; ")"; ","; "."];;
-  
-let rec parse_gwmlrc (strm__ : _ Stream.t) =
-  match
-    try Some (parse_id strm__) with
-      Stream.Failure -> None
-  with
-    Some id ->
-      begin match Stream.peek strm__ with
-        Some (Kwd "=") ->
-          Stream.junk strm__;
-          let v =
-            try parse_option strm__ with
-              Stream.Failure -> raise (Stream.Error "")
-          in
-          let eof =
-            try parse_gwmlrc strm__ with
-              Stream.Failure -> raise (Stream.Error "")
-          in
-          (id, v) :: eof
-      | _ -> raise (Stream.Error "")
-      end
-  | _ -> []
-and parse_option (strm__ : _ Stream.t) =
-  match Stream.peek strm__ with
-    Some (Kwd "{") ->
-      Stream.junk strm__;
-      let v =
-        try parse_gwmlrc strm__ with
-          Stream.Failure -> raise (Stream.Error "")
-      in
-      begin match Stream.peek strm__ with
-        Some (Kwd "}") -> Stream.junk strm__; Module v
-      | _ -> raise (Stream.Error "")
-      end
-  | Some (Ident s) -> Stream.junk strm__; StringValue s
-  | Some (String s) -> Stream.junk strm__; StringValue s
-  | Some (Int i) -> Stream.junk strm__; IntValue i
-  | Some (Float f) -> Stream.junk strm__; FloatValue f
-  | Some (Char c) ->
-      Stream.junk strm__;
-      StringValue (let s = String.create 1 in s.[0] <- c; s)
-  | Some (Kwd "[") ->
-      Stream.junk strm__;
-      let v =
-        try parse_list strm__ with
-          Stream.Failure -> raise (Stream.Error "")
-      in
-      List v
-  | Some (Kwd "(") ->
-      Stream.junk strm__;
-      let v =
-        try parse_list strm__ with
-          Stream.Failure -> raise (Stream.Error "")
-      in
-      List v
-  | _ -> raise Stream.Failure
-and parse_id (strm__ : _ Stream.t) =
-  match Stream.peek strm__ with
-    Some (Ident s) -> Stream.junk strm__; s
-  | Some (String s) -> Stream.junk strm__; s
-  | _ -> raise Stream.Failure
-and parse_list (strm__ : _ Stream.t) =
-  match Stream.peek strm__ with
-    Some (Kwd ";") ->
-      Stream.junk strm__;
-      begin try parse_list strm__ with
-        Stream.Failure -> raise (Stream.Error "")
-      end
-  | Some (Kwd ",") ->
-      Stream.junk strm__;
-      begin try parse_list strm__ with
-        Stream.Failure -> raise (Stream.Error "")
-      end
-  | Some (Kwd ".") ->
-      Stream.junk strm__;
-      begin try parse_list strm__ with
-        Stream.Failure -> raise (Stream.Error "")
-      end
-  | _ ->
-      match
-        try Some (parse_option strm__) with
-          Stream.Failure -> None
-      with
-        Some v ->
-          let t =
-            try parse_list strm__ with
-              Stream.Failure -> raise (Stream.Error "")
-          in
-          v :: t
-      | _ ->
-          match Stream.peek strm__ with
-            Some (Kwd "]") -> Stream.junk strm__; []
-          | Some (Kwd ")") -> Stream.junk strm__; []
-          | _ -> raise Stream.Failure
-;;
-
-let exec_hooks o =
-  List.iter
-    (fun f ->
-       try f () with
-         _ -> ())
-    o.option_hooks
-;;  
-
-let exec_chooks o =
-  List.iter
-    (fun f ->
-       try f o with
-         _ -> ())
-    o.option_class.class_hooks
-;;  
-  
-let really_load filename options =
-  let temp_file = filename ^ ".tmp" in
-  if Sys.file_exists temp_file then begin
-      Printf.printf 
-        "File %s exists\n" temp_file;
-      Printf.printf 
-        "An error may have occurred during previous configuration save.\n";
-      Printf.printf 
-        "Please, check your configurations files, and rename/remove this file\n";
-      Printf.printf "before restarting";
-      print_newline ();
-      exit 1
-    end 
-  else
-    let ic = open_in filename in
-    let s = Stream.of_channel ic in
-    try
-      let stream = lexer s in
-      let list =
-	try parse_gwmlrc stream with
-          e ->
-            Printf.printf "At pos %d/%d" (Stream.count s) (Stream.count stream);
-            print_newline ();
-            raise e
-      in
-      List.iter
-	(fun o ->
-          try
-            o.option_value <-
-              o.option_class.from_value (find_value o.option_name list);
-            exec_chooks o;
-            exec_hooks o
-          with
-            e ->
-             ()
-	)
-	options;
-      list
-    with
-      e ->
-	Printf.printf "Error %s in %s" (Printexc.to_string e) filename;
-	print_newline ();
-	[]
-;;
-      
-let load opfile =
-  try opfile.file_rc <- really_load opfile.file_name opfile.file_options with
-    Not_found -> 
-      Printf.printf "No %s found" opfile.file_name; print_newline ()
-;;
-
-let append opfile filename =
-  try opfile.file_rc <-
-    really_load filename opfile.file_options @ opfile.file_rc with
-    Not_found -> 
-      Printf.printf "No %s found" filename; print_newline ()
-;;
-      
-let ( !! ) o = o.option_value;;
-let ( =:= ) o v = o.option_value <- v; exec_chooks o; exec_hooks o;;
-    
-let value_to_string v =
-  match v with
-    StringValue s -> s
-  | IntValue i -> string_of_int i
-  | FloatValue f -> string_of_float f
-  | _ -> failwith "Flags. not a string option"
-;;
-      
-let string_to_value s = StringValue s;;
-  
-let value_to_int v =
-  match v with
-    StringValue s -> int_of_string s
-  | IntValue i -> i
-  | _ -> failwith "Flags. not an int option"
-;;
-
-let int_to_value i = IntValue i;;
-
-(* The Pervasives version is too restrictive *)
-let bool_of_string s =
-  match String.lowercase s with
-    "true" -> true
-  | "false" -> false
-  | "yes" -> true
-  | "no" -> false
-  | "y" -> true
-  | "n" -> false
-  | _ -> invalid_arg "bool_of_string"
-;;
-
-let value_to_bool v =
-  match v with
-    StringValue s -> bool_of_string s
-  | IntValue v when v = 0 -> false
-  | IntValue v when v = 1 -> true
-  | _ -> failwith "Flags. not a bool option"
-;;
-let bool_to_value i = StringValue (string_of_bool i);;
-
-let value_to_float v =
-  match v with
-    StringValue s -> float_of_string s
-  | FloatValue f -> f
-  | _ -> failwith "Flags. not a float option"
-;; 
-
-let float_to_value i = FloatValue i;;
-
-let value_to_string2 v =
-  match v with
-    List [s1; s2] | SmallList [s1;s2] -> 
-      value_to_string s1, value_to_string s2
-  | _ -> failwith "Flags. not a string2 option"
-;;
-
-let string2_to_value (s1, s2) = SmallList [StringValue s1; StringValue s2];;
-
-let value_to_list v2c v =
-  match v with
-    List l | SmallList l -> List.rev (List.rev_map v2c l)
-  | StringValue s -> failwith (Printf.sprintf 
-        "Flags. not a list option (StringValue [%s])" s)
-  | FloatValue _ -> failwith "Flags. not a list option (FloatValue)"
-  | IntValue _ -> failwith "Flags. not a list option (IntValue)"
-  | Module _ -> failwith "Flags. not a list option (Module)"
-;;
-
-let list_to_value c2v l =
-  List
-    (List.fold_right
-      (fun v list ->
-          try c2v v :: list with
-            _ -> list)
-       l [])
-;;
-  
-let smalllist_to_value c2v l =
-  SmallList
-    (List.fold_right
-       (fun v list ->
-          try c2v v :: list with
-            _ -> list)
-       l [])
-;;
-
-let string_option =
-  define_option_class "String" value_to_string string_to_value
-;;
-let color_option =
-  define_option_class "Color" value_to_string string_to_value
-;;
-let font_option = define_option_class "Font" value_to_string string_to_value;;
-
-let int_option = define_option_class "Int" value_to_int int_to_value;;
-
-let bool_option = define_option_class "Bool" value_to_bool bool_to_value;;
-let float_option = define_option_class "Float" value_to_float float_to_value;;
-
-let string2_option =
-  define_option_class "String2" value_to_string2 string2_to_value
-;;
-
-let list_option cl =
-  define_option_class (cl.class_name ^ " List") (value_to_list cl.from_value)
-    (list_to_value cl.to_value)
-;;
-
-let smalllist_option cl =
-  define_option_class (cl.class_name ^ " List") (value_to_list cl.from_value)
-    (smalllist_to_value cl.to_value)
-;;
-
-let to_value cl = cl.to_value;;
-let from_value cl = cl.from_value;;
-  
-let value_to_sum l v =
-  match v with
-    StringValue s -> List.assoc s l
-  | _ -> failwith "Flags. not a sum option"
-;;
-  
-let sum_to_value l v = StringValue (List.assq v l);;
-  
-let sum_option l =
-  let ll = List.map (fun (a1, a2) -> a2, a1) l in
-  define_option_class "Sum" (value_to_sum l) (sum_to_value ll)
-;;
-
-let exit_exn = Exit;;
-let safe_string s =
-  if s = "" then "\"\""
-  else
-    try
-      match s.[0] with
-        'a'..'z' | 'A'..'Z' ->
-          for i = 1 to String.length s - 1 do
-            match s.[i] with
-              'a'..'z' | 'A'..'Z' | '_' | '0'..'9' -> ()
-            | _ -> raise exit_exn
-          done;
-          s
-      | _ ->
-          if string_of_int (int_of_string s) = s ||
-             string_of_float (float_of_string s) = s then
-            s
-          else raise exit_exn
-    with
-      _ -> Printf.sprintf "\"%s\"" (String.escaped s)
-;;
-
-let with_help = ref false;;
-      
-let rec save_module indent oc list =
-  let subm = ref [] in
-  List.iter
-    (fun (name, help, value) ->
-       match name with
-         [] -> assert false
-       | [name] ->
-           if !with_help && help <> "" then
-             Printf.fprintf oc "(* %s *)\n" help;
-           Printf.fprintf oc "%s %s = " indent (safe_string name);
-           save_value indent oc value;
-           Printf.fprintf oc "\n"
-       | m :: tail ->
-           let p =
-             try List.assoc m !subm with
-               _ -> let p = ref [] in subm := (m, p) :: !subm; p
-           in
-           p := (tail, help, value) :: !p)
-    list;
-  List.iter
-    (fun (m, p) ->
-       Printf.fprintf oc "%s %s = {\n" indent (safe_string m);
-       save_module (indent ^ "  ") oc !p;
-       Printf.fprintf oc "%s}\n" indent)
-    !subm
-and save_list indent oc list =
-  match list with
-    [] -> ()
-  | [v] -> save_value indent oc v
-  | v :: tail ->
-      save_value indent oc v; Printf.fprintf oc ", "; save_list indent oc tail
-and save_list_nl indent oc list =
-  match list with
-    [] -> ()
-  | [v] -> Printf.fprintf oc "\n%s" indent; save_value indent oc v
-  | v :: tail ->
-      Printf.fprintf oc "\n%s" indent;
-      save_value indent oc v;
-      Printf.fprintf oc ";";
-      save_list_nl indent oc tail
-and save_value indent oc v =
-  match v with
-    StringValue s -> Printf.fprintf oc "%s" (safe_string s)
-  | IntValue i -> Printf.fprintf oc "%d" i
-  | FloatValue f -> Printf.fprintf oc "%f" f
-  | List l ->
-      Printf.fprintf oc "[";
-      save_list_nl (indent ^ "  ") oc l;
-      Printf.fprintf oc "]"
-  | SmallList l ->
-      Printf.fprintf oc "(";
-      save_list (indent ^ "  ") oc l;
-      Printf.fprintf oc ")"
-  | Module m -> 
-      Printf.fprintf oc "{";
-      save_module_fields (indent ^ "  ") oc m;
-      Printf.fprintf oc "}"
-      
-and save_module_fields indent oc m =
-  match m with
-    [] -> ()
-  | (name, v) :: tail ->
-      Printf.fprintf oc "%s %s = " indent (safe_string name);
-      save_value indent oc v;
-      Printf.fprintf oc "\n";
-      save_module_fields indent oc tail
-;;
-    
-let save opfile =
-  let filename = opfile.file_name in
-  let temp_file = filename ^ ".tmp" in
-  let old_file = filename ^ ".old" in
-  let oc = open_out temp_file in
-  save_module "" oc
-    (List.map
-      (fun o ->
-        o.option_name, o.option_help,
-        (try 
-            o.option_class.to_value o.option_value 
-          with
-            e ->
-              Printf.printf "Error while saving option \"%s\": %s"
-                (try List.hd o.option_name with
-                  _ -> "???")
-              (Printexc.to_string e);
-              print_newline ();
-              StringValue ""))
-    (List.rev opfile.file_options));
-  if not opfile.file_pruned then begin
-      Printf.fprintf oc
-        "\n(*\n The following options are not used (errors, obsolete, ...) \n*)\n";
-      List.iter
-        (fun (name, value) ->
-          try
-            List.iter
-              (fun o ->
-                match o.option_name with
-                  n :: _ -> if n = name then raise Exit
-                | _ -> ())
-            opfile.file_options;
-            Printf.fprintf oc "%s = " (safe_string name);
-            save_value "  " oc value;
-            Printf.fprintf oc "\n"
-          with
-            _ -> ())
-      opfile.file_rc;
-    end;
-  close_out oc;
-  (try Sys.rename filename old_file with _ -> ());
-  (try Sys.rename temp_file filename with _ -> ())
-;;
-
-let save_with_help opfile =
-  with_help := true;
-  begin try save opfile with
-    _ -> ()
-  end;
-  with_help := false
-;;
-  
-let option_hook option f = option.option_hooks <- f :: option.option_hooks;;
-  
-let class_hook option_class f =
-  option_class.class_hooks <- f :: option_class.class_hooks
-;;
-
-let rec iter_order f list =
-  match list with
-    [] -> ()
-  | v :: tail -> f v; iter_order f tail
-;;
-  
-let help oc opfile =
-  List.iter
-    (fun o ->
-       Printf.fprintf oc "OPTION \"";
-       begin match o.option_name with
-         [] -> Printf.fprintf oc "???"
-       | [name] -> Printf.fprintf oc "%s" name
-       | name :: tail ->
-           Printf.fprintf oc "%s" name;
-           iter_order (fun name -> Printf.fprintf oc ":%s" name) o.option_name
-       end;
-       Printf.fprintf oc "\" (TYPE \"%s\"): %s\n   CURRENT: \n"
-         o.option_class.class_name o.option_help;
-       begin try
-         save_value "" oc (o.option_class.to_value o.option_value)
-       with
-         _ -> ()
-       end;
-       Printf.fprintf oc "\n")
-    opfile.file_options;
-  flush oc
-;;
-  
-    
-let tuple2_to_value (c1, c2) (a1, a2) =
-  SmallList [to_value c1 a1; to_value c2 a2]
-;;
-  
-let value_to_tuple2 (c1, c2) v =
-  match v with
-    List [v1; v2] -> from_value c1 v1, from_value c2 v2
-  | SmallList [v1; v2] -> from_value c1 v1, from_value c2 v2
-  | List l | SmallList l ->
-      Printf.printf "list of %d" (List.length l);
-      print_newline ();
-      failwith "Flags. not a tuple2 list option"
-  | _ -> failwith "Flags. not a tuple2 option"
-;;
-  
-let tuple2_option p =
-  define_option_class "tuple2_option" (value_to_tuple2 p) (tuple2_to_value p)
-;;
-  
-let tuple3_to_value (c1, c2, c3) (a1, a2, a3) =
-  SmallList [to_value c1 a1; to_value c2 a2; to_value c3 a3]
-;;
-let value_to_tuple3 (c1, c2, c3) v =
-  match v with
-    List [v1; v2; v3] -> from_value c1 v1, from_value c2 v2, from_value c3 v3
-  | SmallList [v1; v2; v3] ->
-      from_value c1 v1, from_value c2 v2, from_value c3 v3
-  | _ -> failwith "Flags. not a tuple3 option"
-;;
-      
-let tuple3_option p =
-  define_option_class "tuple3_option" (value_to_tuple3 p) (tuple3_to_value p)
-;;
-
-let tuple4_to_value (c1, c2, c3, c4) (a1, a2, a3, a4) =
-  SmallList [to_value c1 a1; to_value c2 a2; to_value c3 a3; to_value c4 a4]
-;;
-let value_to_tuple4 (c1, c2, c3, c4) v =
-  match v with
-    List [v1; v2; v3; v4] -> 
-      (from_value c1 v1, from_value c2 v2, from_value c3 v3, from_value c4 v4)
-  | SmallList [v1; v2; v3; v4] ->
-      (from_value c1 v1, from_value c2 v2, from_value c3 v3, from_value c4 v4)
-  | _ -> failwith "Flags. not a tuple4 option"
-;;
-      
-let tuple4_option p =
-  define_option_class "tuple4_option" (value_to_tuple4 p) (tuple4_to_value p)
-;;
-
-
-let shortname o = String.concat ":" o.option_name;;
-let get_class o = o.option_class;;
-let get_help o =
-  let help = o.option_help in if help = "" then "No Help Available" else help
-;;
-
-
-let simple_options opfile =
-  let list = ref [] in
-  List.iter (fun o ->
-      match o.option_name with
-        [] | _ :: _ :: _ -> ()
-      | [name] ->
-          match o.option_class.to_value o.option_value with
-            Module _ | SmallList _ | List _ -> 
-              begin
-                match o.string_wrappers with
-                  None -> ()
-                | Some (to_string, from_string) ->
-                    list := (name, to_string o.option_value) :: !list   
-              end
-          | v -> 
-              list := (name, value_to_string v) :: !list
-  ) opfile.file_options;
-  !list
-
-let get_option opfile name =
-  let rec iter name list = 
-    match list with 
-      [] -> raise Not_found
-    | o :: list ->
-        if o.option_name = name then o
-        else iter name list
-  in
-  iter [name] opfile.file_options
-  
-  
-let set_simple_option opfile name v =
-  let o = get_option opfile name in
-  begin
-    match o.string_wrappers with
-      None ->
-        o.option_value <- o.option_class.from_value (string_to_value v);
-    | Some (_, from_string) -> 
-        o.option_value <- from_string v
-  end;
-  exec_chooks o; exec_hooks o;;
-    
-let get_simple_option opfile name =
-  let o = get_option opfile name in
-  match o.string_wrappers with
-    None ->
-      value_to_string (o.option_class.to_value o.option_value)
-  | Some (to_string, _) -> 
-      to_string o.option_value
-  
-let set_option_hook opfile name hook =
-  let o = get_option opfile name in
-  o.option_hooks <- hook :: o.option_hooks
-  
-let set_string_wrappers o to_string from_string =
-  o.string_wrappers <- Some (to_string, from_string)
-
-let simple_args opfile =
-  List.map (fun (name, v) ->
-      ("-" ^ name), 
-      Arg.String (set_simple_option opfile name), 
-      (Printf.sprintf "<string> : \t%s (current: %s)"
-          (get_option opfile name).option_help
-          v)
-  ) (simple_options opfile)
diff --git a/ide/utils/uoptions.mli b/ide/utils/uoptions.mli
deleted file mode 100644
index a323ac60..00000000
--- a/ide/utils/uoptions.mli
+++ /dev/null
@@ -1,148 +0,0 @@
-(**************************************************************************)
-(*                   Cameleon                                             *)
-(*                                                                        *)
-(*      Copyright (C) 2002 Institut National de Recherche en Informatique et   *)
-(*      en Automatique. All rights reserved.                              *)
-(*                                                                        *)
-(*      This program is free software; you can redistribute it and/or modify  *)
-(*      it under the terms of the GNU General Public License as published by  *)
-(*      the Free Software Foundation; either version 2 of the License, or  *)
-(*      any later version.                                                *)
-(*                                                                        *)
-(*      This program is distributed in the hope that it will be useful,   *)
-(*      but WITHOUT ANY WARRANTY; without even the implied warranty of    *)
-(*      MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     *)
-(*      GNU General Public License for more details.                      *)
-(*                                                                        *)
-(*      You should have received a copy of the GNU General Public License  *)
-(*      along with this program; if not, write to the Free Software       *)
-(*      Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA          *)
-(*      02111-1307  USA                                                   *)
-(*                                                                        *)
-(*      Contact: Maxence.Guesdon@inria.fr                                *)
-(**************************************************************************)
-
-(**
- This module implements a simple mechanism to handle program options files.
-  An options file is defined as a set of [variable = value] lines,
-  where value can be a simple string, a list of values (between brackets
-or parentheses) or a set of [variable = value] lines between braces.
-The option file is automatically loaded and saved, and options are
-manipulated inside the program as easily as references. 
-
-   Code from Fabrice Le Fessant.
-*)
-
-type 'a option_class
-(** The abstract type for a class of options. A class is a set of options
-which use the same conversion functions from loading and saving.*)
-  
-type 'a option_record
-(** The abstract type for an option *)
-
-type options_file
-
-val create_options_file : string -> options_file
-val set_options_file : options_file -> string -> unit
-val prune_file : options_file -> unit  
-
-(** {2 Operations on option files} *)
-  
-val load : options_file -> unit
-(** [load file] loads the option file. All options whose value is specified
-   in the option file are updated. *)
-  
-val append : options_file -> string -> unit
-(** [append filename] loads the specified option file. All options whose 
-value is specified in this file are updated. *)
-  
-val save : options_file -> unit
-(** [save file] saves all the options values to the option file. *)
-
-val save_with_help : options_file -> unit
-(** [save_with_help ()] saves all the options values to the option file,
-   with the help provided for each option. *)
-  
-(** {2  Creating options} *)  
-
-val define_option : options_file ->
-  string list ->  string -> 'a option_class -> 'a -> 'a option_record
-val option_hook : 'a option_record -> (unit -> unit) -> unit
-    
-val string_option : string option_class
-val color_option : string option_class
-val font_option : string option_class
-val int_option : int option_class
-val bool_option : bool option_class
-val float_option : float option_class
-val string2_option : (string * string) option_class
-  
-  (* parameterized options *)
-val list_option : 'a option_class -> 'a list option_class
-val smalllist_option : 'a option_class -> 'a list option_class
-val sum_option : (string * 'a) list -> 'a option_class
-val tuple2_option :  
-  'a option_class * 'b option_class -> ('a * 'b) option_class
-val tuple3_option : 'a option_class * 'b option_class * 'c option_class ->
-  ('a * 'b * 'c) option_class
-val tuple4_option : 
-    'a option_class * 'b option_class * 'c option_class * 'd option_class ->
-  ('a * 'b * 'c * 'd) option_class
-
-(** {2  Using options} *)
-  
-val ( !! ) : 'a option_record -> 'a
-val ( =:= ) : 'a option_record -> 'a -> unit
-
-val shortname : 'a option_record -> string
-val get_help : 'a option_record -> string  
-  
-(** {2 Creating new option classes} *)
-
-val get_class : 'a option_record -> 'a option_class
-
-val class_hook : 'a option_class -> ('a option_record -> unit) -> unit
-
-type option_value =
-  Module of option_module
-| StringValue of  string
-| IntValue of int
-| FloatValue of float
-| List of option_value list
-| SmallList of option_value list
-  
-and option_module =
-  (string * option_value) list
-
-val define_option_class :
-  string -> (option_value -> 'a) -> ('a -> option_value) -> 'a option_class
-
-val to_value : 'a option_class -> 'a -> option_value
-val from_value : 'a option_class -> option_value -> 'a
-  
-val value_to_string : option_value -> string
-val string_to_value : string -> option_value
-val value_to_int : option_value -> int
-val int_to_value : int -> option_value
-val bool_of_string : string -> bool
-val value_to_bool : option_value -> bool
-val bool_to_value : bool -> option_value
-val value_to_float : option_value -> float
-val float_to_value : float -> option_value
-val value_to_string2 : option_value -> string * string
-val string2_to_value : string * string -> option_value
-val value_to_list : (option_value -> 'a) -> option_value -> 'a list
-val list_to_value : ('a -> option_value) -> 'a list -> option_value
-val smalllist_to_value : ('a -> option_value) -> 'a list -> option_value
-
-val set_simple_option : options_file -> string -> string -> unit
-val simple_options : options_file -> (string * string) list
-val get_simple_option : options_file -> string -> string
-val set_option_hook : options_file -> string -> (unit -> unit) -> unit
-  
-val set_string_wrappers : 'a option_record -> 
-  ('a -> string) -> (string -> 'a) -> unit
-
-(** {2 Other functions} *)
-
-val simple_args : options_file -> (string * Arg.spec * string) list