Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

37 files changed, 2189 insertions, 1085 deletions

diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml
index cca788c2..1b018015 100644
--- a/ide/blaster_window.ml
+++ b/ide/blaster_window.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: blaster_window.ml,v 1.5.2.1 2004/07/16 19:30:19 herbelin Exp $ *)
+(* $Id: blaster_window.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Gobject.Data
 open Ideutils
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 42b65048..1f40e057 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command_windows.ml,v 1.13.2.1 2004/07/16 19:30:19 herbelin Exp $ *)
+(* $Id: command_windows.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 class command_window () = 
   let window = GWindow.window 
diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index 6028c818..3a5f0d60 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: command_windows.mli,v 1.1.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
+(*i $Id: command_windows.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
 class command_window :
   unit ->
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 1c0720d1..7722e99a 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: config_lexer.mll,v 1.4.2.1 2004/07/16 19:30:19 herbelin Exp $ *)
+(* $Id: config_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 {
 
diff --git a/ide/config_parser.mly b/ide/config_parser.mly
index 48005efe..80cba27b 100644
--- a/ide/config_parser.mly
+++ b/ide/config_parser.mly
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (***********************************************************************/
 
-/* $Id: config_parser.mly,v 1.2.2.1 2004/07/16 19:30:20 herbelin Exp $ */
+/* $Id: config_parser.mly 5920 2004-07-16 20:01:26Z herbelin $ */
 
 %{
 
diff --git a/ide/coq.ico b/ide/coq.ico
index 390065bc..b99f6399 100644
--- a/ide/coq.ico
+++ b/ide/coq.ico
diff --git a/ide/coq.ml b/ide/coq.ml
index 31f9829b..31c2f792 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml,v 1.38.2.2 2005/11/16 17:22:38 barras Exp $ *)
+(* $Id: coq.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
 
 open Vernac
 open Vernacexpr
@@ -249,7 +249,7 @@ type goal = hyp list * concl
 let prepare_hyp sigma env ((i,c,d) as a) =
   env, sigma,
   ((i,string_of_id i),c,d), 
-  (msg (pr_var_decl env a), msg (prterm_env_at_top env d))
+  (msg (pr_var_decl env a), msg (pr_lconstr_env_at_top env d))
 
 let prepare_hyps sigma env =
   assert (rel_context env = []);
@@ -263,7 +263,7 @@ let prepare_hyps sigma env =
 let prepare_goal sigma g =
   let env = evar_env g in
   (prepare_hyps sigma env,
-   (env, sigma, g.evar_concl, msg (prterm_env_at_top env g.evar_concl)))
+   (env, sigma, g.evar_concl, msg (pr_lconstr_env_at_top env g.evar_concl)))
 
 let get_current_goals () = 
     let pfts = get_pftreestate () in
@@ -280,7 +280,7 @@ let print_no_goal () =
     let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
     assert (gls = []);
     let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in
-    msg (Proof_trees.pr_subgoals_existential sigma gls)
+    msg (Printer.pr_subgoals sigma gls)
 
 
 type word_class = Normal | Kwd | Reserved
@@ -329,8 +329,8 @@ type reset_info = NoReset | Reset of Names.identifier * bool ref
 let compute_reset_info = function 
   | VernacDefinition (_, (_,id), DefineBody _, _) 
   | VernacBeginSection (_,id) 
-  | VernacDefineModule ((_,id), _, _, _) 
-  | VernacDeclareModule ((_,id), _, _, _)
+  | VernacDefineModule (_,(_,id), _, _, _) 
+  | VernacDeclareModule (_,(_,id), _, _)
   | VernacDeclareModuleType ((_,id), _, _)
   | VernacAssumption (_, (_,((_,id)::_,_))::_)
   | VernacInductive (_, ((_,id),_,_,_,_) :: _) ->
@@ -432,10 +432,8 @@ let make_cases s =
   let glob_ref = Nametab.locate qualified_name in
   match glob_ref with
     | Libnames.IndRef i -> 
-	let _,
-	{
-	  Declarations.mind_nparams = np ;
-	  Declarations.mind_consnames = carr ;
+	let {Declarations.mind_nparams = np},
+	{Declarations.mind_consnames = carr ;
 	 Declarations.mind_nf_lc = tarr } 
 	= Global.lookup_inductive i 
 	in
diff --git a/ide/coq.mli b/ide/coq.mli
index c1dfd847..eaa32068 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coq.mli,v 1.14.2.3 2005/01/21 17:21:33 herbelin Exp $ i*)
+(*i $Id: coq.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/ide/coq.png b/ide/coq.png
index 011203f7..2e5bdcd6 100644
--- a/ide/coq.png
+++ b/ide/coq.png
diff --git a/ide/coq2.ico b/ide/coq2.ico
index 36964902..bc1732fd 100755
--- a/ide/coq2.ico
+++ b/ide/coq2.ico
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 1169d438..30d99f5b 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_commands.ml,v 1.15.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: coq_commands.ml 7102 2005-06-03 13:14:27Z coq $ *)
 
 let commands = [
   [(* "Abort"; *)
@@ -22,6 +22,7 @@ let commands = [
    "Add Rec ML Path";
    "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. ";
    "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ].";
+   "Add Relation";
    "Add Setoid";
    "Axiom";];
   [(* "Back"; *) ];
@@ -63,7 +64,7 @@ let commands = [
    "Hint Unfold";
    "Hypothesis";];
   ["Identity Coercion";
-   "Implicits";
+   "Implicit Arguments";
    "Inductive";
    "Infix";
    ];
@@ -173,6 +174,8 @@ let state_preserving = [
   "Print Module Type";
   "Print Modules";
   "Print Proof";
+  "Print Rewrite HintDb";
+  "Print Setoids";
   "Print Scope";
   "Print Scopes.";
   "Print Section";
@@ -196,6 +199,7 @@ let state_preserving = [
 
   "Show";
   "Show Conjectures";
+  "Show Existentials";
   "Show Implicits";
   "Show Intro";
   "Show Intros";
@@ -207,6 +211,9 @@ let state_preserving = [
   "Test Printing Let";
   "Test Printing Synth";
   "Test Printing Wildcard";
+
+  "Whelp Hint";
+  "Whelp Locate";
 ]
 
 
diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml
index 4dd20b47..92d2de78 100644
--- a/ide/coq_tactics.ml
+++ b/ide/coq_tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_tactics.ml,v 1.2.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: coq_tactics.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 let tactics = [
   "Abstract";
diff --git a/ide/coq_tactics.mli b/ide/coq_tactics.mli
index 962b4d27..05e233eb 100644
--- a/ide/coq_tactics.mli
+++ b/ide/coq_tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coq_tactics.mli,v 1.1.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
+(*i $Id: coq_tactics.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
 val tactics : string list
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index a8179fb9..d79ee950 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml,v 1.99.2.6 2006/01/06 13:22:36 barras Exp $ *)
+(* $Id: coqide.ml 7644 2005-12-13 14:18:13Z narboux $ *)
 
 open Preferences
 open Vernacexpr
@@ -26,7 +26,6 @@ let (proof_view:GText.view option ref) = ref None
 let (_notebook:GPack.notebook option ref) = ref None
 let notebook () = out_some !_notebook
 
-
 (* Tabs contain the name of the edited file and 2 status informations: 
    Saved state + Focused proof buffer *)
 let decompose_tab w = 
@@ -252,7 +251,6 @@ let do_if_not_computing text f x =
     if Mutex.try_lock coq_computing 
     then 
       begin
-	prerr_endline ("Launching thread " ^ text);
 	let w = Blaster_window.blaster_window () in
 	if not (Mutex.try_lock w#lock) then begin 
 	  break ();
@@ -273,7 +271,7 @@ let do_if_not_computing text f x =
 	    Glib.Timeout.remove idle;
 	    prerr_endline "Releasing lock";
 	    Mutex.unlock coq_computing;
-	  with e -> 
+	  with e ->
 	    Glib.Timeout.remove idle;
 	    prerr_endline "Releasing lock (on error)";
 	    Mutex.unlock coq_computing;
@@ -283,6 +281,7 @@ let do_if_not_computing text f x =
     else 
       prerr_endline 
 	"Discarded order (computations are ongoing)" in
+  prerr_endline ("Launching thread " ^ text);
   ignore (Thread.create threaded_task ())
 
 let add_input_view tv = 
@@ -511,8 +510,8 @@ let update_on_end_of_proof id =
 let update_on_end_of_segment id =
   let lookup_section = function 
     | { ast = _, ( VernacBeginSection id'
-		 | VernacDefineModule (id',_,_,None)
-		 | VernacDeclareModule (id',_,_,None)
+		 | VernacDefineModule (_,id',_,_,None)
+		 | VernacDeclareModule (_,id',_,_)
 		 | VernacDeclareModuleType (id',_,None)); 
 	reset_info = Reset (_, r) } 
        when id = id' -> raise Exit
@@ -799,7 +798,7 @@ object(self)
 				 goal_nb
 				 (if goal_nb<=1 then "" else "s"));
 	  List.iter
-	    (fun ((_,_,_,(s,_)) as hyp) -> 
+	    (fun ((_,_,_,(s,_)) as _hyp) -> 
 	       proof_buffer#insert (s^"\n"))
 	    hyps;
 	  proof_buffer#insert (String.make 38 '_' ^ "(1/"^
@@ -944,37 +943,37 @@ object(self)
     let display_output msg =
       self#insert_message (if show_output then msg else "") in
     let display_error e =
-	 let (s,loc) = Coq.process_exn e in
-	 assert (Glib.Utf8.validate s);
-	 self#set_message s;
-	 message_view#misc#draw None;
-	 if localize then 
-	   (match Util.option_app Util.unloc loc with 
-	    | None -> ()
-	    | Some (start,stop) ->
-		let convert_pos = byte_offset_to_char_offset phrase in
-		let start = convert_pos start in
-		let stop = convert_pos stop in
-		let i = self#get_start_of_input in 
-		let starti = i#forward_chars start in
-		let stopi = i#forward_chars stop in
-		input_buffer#apply_tag_by_name "error"
-   		  ~start:starti
-		  ~stop:stopi;
-		input_buffer#place_cursor starti) in
+      let (s,loc) = Coq.process_exn e in
+      assert (Glib.Utf8.validate s);
+      self#insert_message s;
+      message_view#misc#draw None;
+      if localize then 
+	(match Util.option_app Util.unloc loc with 
+	  | None -> ()
+	  | Some (start,stop) ->
+	      let convert_pos = byte_offset_to_char_offset phrase in
+	      let start = convert_pos start in
+	      let stop = convert_pos stop in
+	      let i = self#get_start_of_input in 
+	      let starti = i#forward_chars start in
+	      let stopi = i#forward_chars stop in
+	      input_buffer#apply_tag_by_name "error"
+   		~start:starti
+		~stop:stopi;
+	      input_buffer#place_cursor starti) in
     try 
       full_goal_done <- false;
       prerr_endline "Send_to_coq starting now";
       if replace then begin
 	let r,info = Coq.interp_and_replace ("info " ^ phrase) in
-	let msg = read_stdout () in 
-	sync display_output msg;
-	Some r
+	let msg = read_stdout () in
+        sync display_output msg;
+	Some r	
       end else begin
 	let r = Coq.interp verbosely phrase in
-	let msg = read_stdout () in 
-	sync display_output msg;
-	Some r
+	let msg = read_stdout () in
+        sync display_output msg;
+        Some r
       end
     with e ->
       if show_error then sync display_error e;
@@ -1065,8 +1064,8 @@ object(self)
 	!push_info "Coq is computing";
 	input_view#set_editable false;
       end;
-      match self#find_phrase_starting_at self#get_start_of_input with
-        | None ->
+      match self#find_phrase_starting_at self#get_start_of_input with 
+	| None ->
 	    if do_highlight then begin
 	      input_view#set_editable true;
 	      !pop_info ();
@@ -1079,37 +1078,37 @@ object(self)
 	      prerr_endline "process_next_phrase : to_process applied";
 	    end;
 	    prerr_endline "process_next_phrase : getting phrase";
-	    Some((start,stop),start#get_slice ~stop) in
-    let remove_tag (start,stop) =
-      if do_highlight then begin
-	input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
-	input_view#set_editable true;
-	!pop_info ();
-      end in
-    let mark_processed (start,stop) ast =
-      let b = input_buffer in
-      b#move_mark ~where:stop (`NAME "start_of_input");
-      b#apply_tag_by_name "processed" ~start ~stop;
-      if (self#get_insert#compare) stop <= 0 then 
-	begin
-	  b#place_cursor stop;
-	  self#recenter_insert
-	end;
-      let start_of_phrase_mark = `MARK (b#create_mark start) in
-      let end_of_phrase_mark = `MARK (b#create_mark stop) in
-      push_phrase 
-	start_of_phrase_mark 
-	end_of_phrase_mark ast;
-      if display_goals then self#show_goals;
-      remove_tag (start,stop) in
-    begin
-      match sync get_next_phrase () with
-        | None -> false
-        | Some (loc,phrase) ->
-	    (match self#send_to_coq verbosely false phrase true true true with
+            Some((start,stop),start#get_slice ~stop) in
+      let remove_tag (start,stop) =
+	if do_highlight then begin
+	  input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
+	  input_view#set_editable true;
+	  !pop_info ();
+	end in
+      let mark_processed (start,stop) ast =
+        let b = input_buffer in
+	b#move_mark ~where:stop (`NAME "start_of_input");
+	b#apply_tag_by_name "processed" ~start ~stop;
+	if (self#get_insert#compare) stop <= 0 then 
+	  begin
+	    b#place_cursor stop;
+	    self#recenter_insert
+	  end;
+	let start_of_phrase_mark = `MARK (b#create_mark start) in
+	let end_of_phrase_mark = `MARK (b#create_mark stop) in
+	push_phrase 
+	  start_of_phrase_mark 
+	  end_of_phrase_mark ast;
+	if display_goals then self#show_goals;
+        remove_tag (start,stop) in
+      begin
+        match sync get_next_phrase () with
+            None -> false
+          | Some (loc,phrase) ->
+            (match self#send_to_coq verbosely false phrase true true true with
 	      | Some ast -> sync (mark_processed loc) ast; true
 	      | None -> sync remove_tag loc; false)
-    end
+      end
     
   method insert_this_phrase_on_success 
     show_output show_msg localize coqphrase insertphrase = 
@@ -1127,37 +1126,37 @@ object(self)
       let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
       push_phrase start_of_phrase_mark end_of_phrase_mark ast;
       self#show_goals;
-      (*Auto insert save on success...
+      (*Auto insert save on success... 
       try (match Coq.get_current_goals () with 
-	  | [] ->  
+	| [] ->  
 	    (match self#send_to_coq "Save.\n" true true true with
-	    | Some ast -> 
-	      begin
-	        let stop = self#get_start_of_input in
-	        if stop#starts_line then
-	          input_buffer#insert ~iter:stop "Save.\n"
-	        else input_buffer#insert ~iter:stop "\nSave.\n"; 
-	        let start = self#get_start_of_input in
-	        input_buffer#move_mark ~where:stop (`NAME "start_of_input");
-	        input_buffer#apply_tag_by_name "processed" ~start ~stop;
-	        if (self#get_insert#compare) stop <= 0 then 
-	          input_buffer#place_cursor stop;
-	        let start_of_phrase_mark =
-                  `MARK (input_buffer#create_mark start) in
-	        let end_of_phrase_mark =
-                  `MARK (input_buffer#create_mark stop) in
-	        push_phrase start_of_phrase_mark end_of_phrase_mark ast
-	      end
-	    | None -> ())
-	  | _ -> ())
-	with _ -> ()*) in
+	      | Some ast -> 
+	          begin
+                    let stop = self#get_start_of_input in
+	            if stop#starts_line then
+	              input_buffer#insert ~iter:stop "Save.\n"
+	            else input_buffer#insert ~iter:stop "\nSave.\n"; 
+	            let start = self#get_start_of_input in
+	            input_buffer#move_mark ~where:stop (`NAME"start_of_input");
+	            input_buffer#apply_tag_by_name "processed" ~start ~stop;
+	            if (self#get_insert#compare) stop <= 0 then 
+	              input_buffer#place_cursor stop;
+	            let start_of_phrase_mark =
+                      `MARK (input_buffer#create_mark start) in
+	            let end_of_phrase_mark =
+                      `MARK (input_buffer#create_mark stop) in
+	            push_phrase start_of_phrase_mark end_of_phrase_mark ast
+	          end
+	      | None -> ())
+	| _ -> ())
+      with _ -> ()*) in
     match self#send_to_coq false false coqphrase show_output show_msg localize with
-    | Some ast -> sync mark_processed ast; true
-    | None ->
-        sync 
-          (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
-          ();
-	false
+      | Some ast -> sync mark_processed ast; true
+      | None ->
+          sync
+            (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
+            ();
+	  false
 
   method process_until_iter_or_error stop =
     let stop' = `OFFSET stop#offset in
@@ -1167,7 +1166,6 @@ object(self)
       input_buffer#apply_tag_by_name ~start ~stop "to_process";
       input_view#set_editable false) ();
     !push_info "Coq is computing";
-(*    process_pending ();*)
     (try 
        while ((stop#compare self#get_start_of_input>=0) 
 	      && (self#process_next_phrase false false false))
@@ -1199,8 +1197,8 @@ object(self)
         ) 
         processed_stack;
       Stack.clear processed_stack;
-      self#clear_message) ();
-    Coq.reset_initial ()
+      self#clear_message)();
+      Coq.reset_initial ()
 
 
   (* backtrack Coq to the phrase preceding iterator [i] *)
@@ -1250,9 +1248,9 @@ object(self)
 	   | None -> synchro () 
 	   | Some n -> try Pfedit.undo n with _ -> synchro ());
           sync (fun _ ->
-	    let start = if is_empty () then input_buffer#start_iter 
-	    else input_buffer#get_iter_at_mark (top ()).stop 
-	    in
+	    let start =
+              if is_empty () then input_buffer#start_iter 
+	      else input_buffer#get_iter_at_mark (top ()).stop in
 	    prerr_endline "Removing (long) processed tag...";
 	    input_buffer#remove_tag_by_name 
 	      ~start 
@@ -1347,6 +1345,7 @@ Please restart and report NOW.";
 
       
   method blaster () = 
+    
     ignore (Thread.create 
 	      (fun () ->  
 		 prerr_endline "Blaster called";
@@ -1354,7 +1353,6 @@ Please restart and report NOW.";
 		 if Mutex.try_lock c#lock then begin
 		   c#clear ();
 		   let current_gls = try get_current_goals () with _ -> [] in
-		   let gls_nb = List.length current_gls in
 		   
 		   let set_goal i (s,t) = 
 		     let gnb = string_of_int i in
@@ -1471,19 +1469,17 @@ Please restart and report NOW.";
       (input_view#event#connect#key_press self#active_keypress_handler);
     prerr_endline "CONNECTED active : ";
     print_id (out_some act_id);
-    let dir = (match 
-		 (out_some ((Vector.get input_views index).analyzed_view))
-		 #filename 
-	       with
-	       | None -> ()
-	       | Some f ->     
-		   if not (is_in_coq_path f) then 
-		     begin
-		       let dir = Filename.dirname f in
-		       ignore (Coq.interp false
-				 (Printf.sprintf "Add LoadPath \"%s\". "  dir))
-		     end)
-    in ()
+    match 
+      (out_some ((Vector.get input_views index).analyzed_view)) #filename 
+    with
+      | None -> ()
+      | Some f ->     
+	  if not (is_in_coq_path f) then 
+	    begin
+	      let dir = Filename.dirname f in
+	      ignore (Coq.interp false
+		(Printf.sprintf "Add LoadPath \"%s\". "  dir))
+	    end
 
       
       
@@ -1733,10 +1729,11 @@ let main files =
 	    ~title:"CoqIde" ()
   in
   (try
-    let icon_image = lib_ide_file "coq2.ico" in
+    let icon_image = lib_ide_file "coq.ico" in
     let icon = GdkPixbuf.from_file icon_image in
     w#set_icon (Some icon)
   with _ -> ());
+
   let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
 
 
@@ -1822,7 +1819,7 @@ let main files =
   let load_f () = 	  
     match select_file ~title:"Load file" () with 
     | None -> ()
-    | (Some f) as fn -> load f
+    | Some f -> load f
   in
   ignore (load_m#connect#activate (load_f));
 
@@ -1896,7 +1893,7 @@ let main files =
   let saveall_f () = 
     Vector.iter
       (function 
-	 | {view = view ; analyzed_view = Some av} as full -> 
+	 | {view = view ; analyzed_view = Some av} -> 
 	     begin match av#filename with 
 	     | None -> ()
 	     | Some f ->
@@ -1919,7 +1916,7 @@ let main files =
   let revert_f () = 
     Vector.iter 
       (function 
-	   {view = view ; analyzed_view = Some av} as full -> 
+	   {view = view ; analyzed_view = Some av} -> 
 	     (try 
 		match av#filename,av#stats with 
 		| Some f,Some stats -> 
@@ -2054,21 +2051,19 @@ let main files =
 	      ignore (get_current_view()).view#clear_undo));
   ignore(edit_f#add_separator ());
   ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
-	   (do_if_not_computing "cut" (sync
-	      (fun () -> GtkSignal.emit_unit
+    (fun () -> GtkSignal.emit_unit
 		 (get_current_view()).view#as_view 
-		 GtkText.View.S.cut_clipboard))));
+		 GtkText.View.S.cut_clipboard));
   ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
 	   (fun () -> GtkSignal.emit_unit
 	      (get_current_view()).view#as_view 
 	      GtkText.View.S.copy_clipboard));
   ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
-	   (do_if_not_computing "paste" (sync 
 	      (fun () -> 
 		 try GtkSignal.emit_unit
 		   (get_current_view()).view#as_view 
 		   GtkText.View.S.paste_clipboard
-		 with _ -> prerr_endline "EMIT PASTE FAILED"))));
+		 with _ -> prerr_endline "EMIT PASTE FAILED"));
   ignore (edit_f#add_separator ());
 
 
@@ -2312,12 +2307,11 @@ let main files =
 *)
   
   ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback:
-	 (do_if_not_computing "complete word" (sync 
 	    (fun () -> 
 	       ignore (
 		 let av = out_some ((get_current_view()).analyzed_view) in 
 		 av#complete_at_offset (av#get_insert)#offset
-	    )))));
+	    )));
 
   ignore(edit_f#add_separator ());
   (* external editor *)
@@ -2349,7 +2343,7 @@ let main files =
   let auto_save_f () = 
     Vector.iter 
       (function 
-	   {view = view ; analyzed_view = Some av} as full -> 
+	   {view = view ; analyzed_view = Some av} -> 
 	     (try 
 		av#auto_save
 	      with _ -> ())
@@ -2402,7 +2396,9 @@ let main files =
   in
 
   let do_or_activate f = 
-    do_if_not_computing "do_or_activate" (do_or_activate (fun av -> f av ; !pop_info();!push_info (Coq.current_status())))
+    do_if_not_computing "do_or_activate"
+      (do_or_activate
+        (fun av -> f av ; !pop_info();!push_info (Coq.current_status())))
   in
 
   let add_to_menu_toolbar text ~tooltip ?key ~callback icon = 
@@ -2472,7 +2468,8 @@ let main files =
     let analyzed_view = out_some current.analyzed_view in
     if analyzed_view#is_active then ignore (f analyzed_view)
   in
-  let do_if_active f = do_if_not_computing "do_if_active" (do_if_active_raw f) in
+  let do_if_active f =
+    do_if_not_computing "do_if_active" (do_if_active_raw f) in
 
 (*
   let blaster_i = 
@@ -2557,9 +2554,8 @@ let main files =
     in
     ignore (factory#add_item menu_text
 	      ~callback:
-	      (do_if_not_computing "simple template" (sync
 		 (fun () -> let {view = view } = get_current_view () in
-		  ignore (view#buffer#insert_interactive text)))))
+		  ignore (view#buffer#insert_interactive text)))
   in
   List.iter 
     (fun l -> 
@@ -2592,17 +2588,15 @@ let main files =
   in
   let add_complex_template (menu_text, text, offset, len, key) =
     (* Templates/Lemma *)
-    let callback = do_if_not_computing "complex template" (sync
-		     (fun () ->
-			let {view = view } = get_current_view () in
-			if view#buffer#insert_interactive text then begin
-			  let iter = view#buffer#get_iter_at_mark `INSERT in
-			  ignore (iter#nocopy#backward_chars offset);
-			  view#buffer#move_mark `INSERT iter;
-			  ignore (iter#nocopy#backward_chars len);
-			  view#buffer#move_mark `SEL_BOUND iter;
-			end))
-    in
+    let callback () =
+      let {view = view } = get_current_view () in
+      if view#buffer#insert_interactive text then begin
+	let iter = view#buffer#get_iter_at_mark `INSERT in
+	ignore (iter#nocopy#backward_chars offset);
+	view#buffer#move_mark `INSERT iter;
+	ignore (iter#nocopy#backward_chars len);
+	view#buffer#move_mark `SEL_BOUND iter;
+      end in
     ignore (templates_factory#add_item menu_text ~callback ?key)
   in
   add_complex_template 
@@ -2671,9 +2665,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
     in
     ignore (factory#add_item menu_text
 	      ~callback:
-	      (do_if_not_computing "simple template" (sync
 		 (fun () -> let {view = view } = get_current_view () in
-		  ignore (view#buffer#insert_interactive text)))))
+		  ignore (view#buffer#insert_interactive text)))
   in
 *)
   ignore (templates_factory#add_separator ());
@@ -2745,6 +2738,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		   ~term 
 		   ())
   in
+  let _ = 
+    queries_factory#add_item "_Whelp Locate" 
+      ~callback:(fun () -> let term = get_current_word () in
+		 (Command_windows.command_window ())#new_command
+		 ~command:"Whelp Locate"
+		   ~term 
+		   ())
+  in
 
   (* Externals *)
   let externals_menu =  factory#add_submenu "_Compile" in
@@ -2954,21 +2955,23 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   (* End of menu *)
 
   (* The vertical Separator between Scripts and Goals *)
-  let hb = GPack.paned `HORIZONTAL  ~border_width:3 ~packing:vbox#add () in
-  _notebook := Some (GPack.notebook ~scrollable:true 
-		       ~packing:hb#add1
+  let hb = GPack.paned `HORIZONTAL  ~border_width:5 ~packing:vbox#add () in
+  let fr_notebook = GBin.frame ~shadow_type:`IN ~packing:hb#add1 () in
+  _notebook := Some (GPack.notebook ~border_width:2 ~show_border:false ~scrollable:true 
+		       ~packing:fr_notebook#add
 		       ());
   let nb = notebook () in
-  let fr2 = GBin.frame ~shadow_type:`ETCHED_OUT ~packing:hb#add2 () in 
-  let hb2 = GPack.paned `VERTICAL  ~border_width:3 ~packing:fr2#add () in
+  let hb2 = GPack.paned `VERTICAL ~packing:hb#add2 () in
+  let fr_a = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in
+  let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in
   let sw2 = GBin.scrolled_window 
 	      ~vpolicy:`AUTOMATIC 
 	      ~hpolicy:`AUTOMATIC
-	      ~packing:(hb2#add) () in
+	      ~packing:(fr_a#add) () in
   let sw3 = GBin.scrolled_window 
 	      ~vpolicy:`AUTOMATIC 
 	      ~hpolicy:`AUTOMATIC
-	      ~packing:(hb2#add) () in
+	      ~packing:(fr_b#add) () in
   let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
   let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) () 
   in
@@ -3181,34 +3184,22 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   let _ = tv3#set_editable false in
   let _ = GtkBase.Widget.add_events tv2#as_widget
 	    [`ENTER_NOTIFY;`POINTER_MOTION] in
-  let _ = tv2#event#connect#motion_notify
-	    ~callback:
-	    (fun e -> 
-	       (do_if_not_computing "motion notify" (sync
-		  (fun e -> 
-		     let win = match tv2#get_window `WIDGET with
-		       | None -> assert false
-		       | Some w -> w
-		     in
-		     let x,y = Gdk.Window.get_pointer_location win in
-		     let b_x,b_y = tv2#window_to_buffer_coords 
-				     ~tag:`WIDGET 
-				     ~x 
-				     ~y 
-		     in
-		     let it = tv2#get_iter_at_location ~x:b_x ~y:b_y in
-		     let tags = it#tags in
-		     List.iter 
-		       ( fun t ->
-			   ignore (GtkText.Tag.event 
-				     t#as_tag
-				     tv2#as_widget
-				     e 
-				     it#as_iter))
-		       tags;
-		     false)) e;
-	       false))
-  in
+  let _ =
+    tv2#event#connect#motion_notify
+      ~callback:
+      (fun e -> 
+	let win = match tv2#get_window `WIDGET with
+	  | None -> assert false
+	  | Some w -> w in
+	let x,y = Gdk.Window.get_pointer_location win in
+	let b_x,b_y = tv2#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
+	let it = tv2#get_iter_at_location ~x:b_x ~y:b_y in
+	let tags = it#tags in
+	List.iter 
+	  (fun t ->
+	    ignore(GtkText.Tag.event t#as_tag tv2#as_widget e it#as_iter))
+	  tags;
+	false) in
   change_font := 
   (fun fd -> 
      tv2#misc#modify_font fd;
@@ -3219,7 +3210,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   );
   let about (b:GText.buffer) =
     (try 
-       let image = lib_ide_file "coq.ico" in
+       let image = lib_ide_file "coq.png" in
        let startup_image = GdkPixbuf.from_file image in
        b#insert_pixbuf ~iter:b#start_iter 
 	 ~pixbuf:startup_image;
@@ -3333,6 +3324,26 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 
 ;;
 
+(* This function check every half of second if GeoProof has send 
+   something on his private clipboard *)
+
+let rec check_for_geoproof_input () = 
+  let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in
+    while true do
+      Thread.delay 0.1;
+      let s = cb_Dr#text in
+	(match s with 
+	     Some s -> 
+	       if s <> "Ack" then
+		 (get_current_view()).view#buffer#insert (s^"\n");
+	       cb_Dr#set_text "Ack"
+	   | None -> ()
+	);
+	(* cb_Dr#clear does not work so i use : *)
+	(* cb_Dr#set_text "Ack" *) 
+    done
+
+
 let start () = 
   let files = Coq.init () in
   ignore_break ();
@@ -3351,9 +3362,10 @@ let start () =
   Command_windows.main ();
   Blaster_window.main 9;
   main files;
+  ignore (Thread.create check_for_geoproof_input ()); 
   while true do 
     try 
-      GtkThread.main ()
+      GtkThread.main ()	
     with
       | Sys.Break -> prerr_endline "Interrupted." ; flush stderr
       | e -> 
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 553426f1..f904c730 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqide.mli,v 1.1.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
+(*i $Id: coqide.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
 (* The CoqIde main module. The following function [start] will parse the
    command line, initialize the load path, load the input 
diff --git a/ide/extract_index.mll b/ide/extract_index.mll
index 4a8c37f1..152ad715 100644
--- a/ide/extract_index.mll
+++ b/ide/extract_index.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: extract_index.mll,v 1.2.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: extract_index.mll 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 {
   open Lexing 
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 7b65bd94..1621e313 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: find_phrase.mll,v 1.8.2.2 2004/10/15 14:50:13 coq Exp $ *)
+(* $Id: find_phrase.mll 6218 2004-10-15 14:27:04Z coq $ *)
 
 {
   exception Lex_error of string
@@ -36,10 +36,12 @@ rule next_phrase = parse
       length := !length + 1; 
       Buffer.add_string buff (Lexing.lexeme lexbuf);
       Buffer.contents buff}
-  | phrase_sep phrase_sep {
-      length := !length + 2; 
-      Buffer.add_string buff (Lexing.lexeme lexbuf);
-      next_phrase lexbuf}
+  | phrase_sep phrase_sep
+      { 
+	length := !length + 2; 
+	Buffer.add_string buff (Lexing.lexeme lexbuf);
+	next_phrase lexbuf
+      }
   | _ 
       { 
 	let c = Lexing.lexeme_char lexbuf 0 in 
diff --git a/ide/highlight.mll b/ide/highlight.mll
index e2a1d0cd..d68cb8a4 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: highlight.mll,v 1.14.2.2 2004/11/27 14:41:43 herbelin Exp $ *)
+(* $Id: highlight.mll 6362 2004-11-27 14:39:35Z herbelin $ *)
 
 {
 
@@ -18,6 +18,33 @@
 
   let comment_start = ref 0
 
+  let is_keyword =
+    let h = Hashtbl.create 97 in
+    List.iter (fun s -> Hashtbl.add h s ())
+      [  "Add" ; "Defined" ; 
+	 "End" ; "Export" ; "Extraction" ; "Hint" ; "Hints" ;
+	 "Implicits" ; "Import" ; 
+	 "Infix" ; "Load" ; "match" ; "Module" ;
+	 "Proof" ; "Qed" ;
+	 "Require" ; "Save" ; "Scheme" ;
+	 "Section" ; "Unset" ;
+	 "Set" ; "Notation"
+      ];
+    Hashtbl.mem h
+
+  let is_declaration =
+    let h = Hashtbl.create 97 in
+    List.iter (fun s -> Hashtbl.add h s ())
+      [ "Lemma" ; "Axiom" ; "CoFixpoint" ; "Definition"  ;
+	"Fixpoint" ; "Hypothesis" ; 
+	"Hypotheses" ; "Axioms" ; "Parameters" ; "Subclass" ;
+	"Remark" ; "Fact" ; "Conjecture" ; "Let" ;
+	"CoInductive" ; "Record" ; "Structure" ;
+	"Inductive" ; "Parameter" ; "Theorem" ; 
+	"Variable" ; "Variables" 
+      ];
+    Hashtbl.mem h
+
 }
 
 let space = 
@@ -28,28 +55,22 @@ let identchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
 let ident = firstchar identchar*
 
-let keyword = 
-  "Add" | "Defined" | 
-  "End" | "Export" | "Extraction" | "Hint" |
-  "Implicits" | "Import" | 
-  "Infix" | "Load" | "match" | "Module" | "Module Type" |
-  "Proof" | "Qed" |
-  "Require" | "Save" | "Scheme" |
-  "Section" | "Unset" |
-  "Set"  
-
 let declaration = 
   "Lemma" | "Axiom" | "CoFixpoint" | "Definition"  |
   "Fixpoint" | "Hypothesis" | 
-  "Hypotheses" | "Axioms" | "Parameters" | "Subclass" |
-  "Remark" | "Fact" | "Conjecture" | "Let" |
-  "CoInductive" | "Record" | "Structure" |
   "Inductive" | "Parameter" | "Theorem" | 
-  "Variable" | "Variables" 
+  "Variable" | "Variables" | "Declare" space+ "Module"
 
 rule next_order = parse
-  | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf }
-  | keyword { lexeme_start lexbuf,lexeme_end lexbuf, "kwd" }
+  | "(*" 
+      { comment_start := lexeme_start lexbuf; comment lexbuf }
+  | "Module Type"
+      { lexeme_start lexbuf,lexeme_end lexbuf, "kwd" }
+  | ident as id 
+      { if is_keyword id then 
+	  lexeme_start lexbuf,lexeme_end lexbuf, "kwd" 
+	else
+	  next_order lexbuf }
   | declaration space+ ident (space* ',' space* ident)* 
             { lexeme_start lexbuf, lexeme_end lexbuf, "decl" } 
   | _    { next_order lexbuf}
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index dc3bcf71..5143358a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ideutils.ml,v 1.30.2.4 2006/01/06 15:40:37 barras Exp $ *)
+(* $Id: ideutils.ml 7609 2005-11-25 17:14:39Z barras $ *)
 
 
 open Preferences
@@ -34,9 +34,9 @@ let prerr_string s =
 
 let lib_ide_file f =
   let coqlib =
-    if !Options.boot then Coq_config.coqtop
-    else
-      System.getenv_else "COQLIB" Coq_config.coqlib in
+    System.getenv_else "COQLIB"
+      (if Coq_config.local || !Options.boot then Coq_config.coqtop
+       else Coq_config.coqlib) in
   Filename.concat (Filename.concat coqlib "ide") f
   
 let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
@@ -61,17 +61,6 @@ let byte_offset_to_char_offset s byte_offset =
     byte_offset - !count_delta
   end
 
-let process_pending () =
-  prerr_endline "Pending process";()
-(*  try 
-    while Glib.Main.pending () do 
-      ignore (Glib.Main.iteration false)
-    done
-  with e -> 
-    prerr_endline "Pending problems : expect a crash very soon";
-    raise e
-*)
-
 let print_id id =
   prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id)))
 
@@ -225,6 +214,25 @@ let async =
 let sync = 
   if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x)
 
+let mutex text f =
+  let m = Mutex.create() in
+  fun x ->
+    if Mutex.try_lock m
+    then 
+      (try
+        prerr_endline ("Got lock on "^text);
+        f x;
+        Mutex.unlock m;
+        prerr_endline ("Released lock on "^text)
+      with e ->
+        Mutex.unlock m;
+        prerr_endline ("Released lock on "^text^" (on error)");
+        raise e)
+    else
+      prerr_endline
+        ("Discarded call for "^text^": computations ongoing")
+
+
 let stock_to_widget ?(size=`DIALOG) s = 
   let img = GMisc.image () 
   in img#set_stock s;
@@ -235,7 +243,8 @@ let rec print_list print fmt = function
   | [x] -> print fmt x
   | x :: r -> print fmt x; print_list print fmt r
 
-
+(* TODO: allow to report output as soon as it comes (user-fiendlier
+   for long commands like make...) *)
 let run_command f c =
   let result = Buffer.create 127 in
   let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index cbdaefb9..3af80f47 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -6,10 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ideutils.mli,v 1.6.2.4 2005/11/25 17:18:28 barras Exp $ i*)
+(*i $Id: ideutils.mli 7608 2005-11-25 17:09:25Z barras $ i*)
 
 val async : ('a -> unit) -> 'a -> unit
 val sync  : ('a -> 'b) -> 'a -> 'b
+
+(* avoid running two instances of a function concurrently *)
+val mutex : string -> ('a -> unit) -> 'a -> unit
+
 val browse : (string -> unit) -> string -> unit
 val browse_keyword : (string -> unit) -> string -> unit
 val byte_offset_to_char_offset : string -> int -> int
@@ -32,7 +36,6 @@ val prerr_endline : string -> unit
 val prerr_string : string -> unit
 val print_id : 'a -> unit
 
-val process_pending : unit -> unit
 val read_stdout : unit -> string
 val revert_timer : GMain.Timeout.id option ref
 val auto_save_timer : GMain.Timeout.id option ref
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 8743b99b..8629fe8e 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: preferences.ml,v 1.27.2.2 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: preferences.ml 7046 2005-05-20 07:38:25Z herbelin $ *)
 
 open Configwin
 open Printf
@@ -123,10 +123,7 @@ let (current:pref ref) =
     modifiers_valid = [`SHIFT; `CONTROL; `MOD1; `MOD4];
 
     
-    cmd_browse = 
-	 if Sys.os_type = "Win32"
-	 then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
-	 else "netscape -remote \"OpenURL(", ")\"";
+    cmd_browse = Options.browser_cmd_fmt;
     cmd_editor = 
 	 if Sys.os_type = "Win32"
 	 then "NOTEPAD ", ""
@@ -269,6 +266,13 @@ let load_pref () =
     prerr_endline ("Could not load preferences ("^
 		   (Printexc.to_string e)^").")
     
+let split_string_format s =
+  try 
+    let i = Util.string_index_from s 0 "%s" in
+    let pre = (String.sub s 0 i) in
+    let post = String.sub s (i+2) (String.length s - i - 2) in
+    pre,post
+  with Not_found -> s,""
 
 let configure () = 
   let cmd_coqc = 
@@ -439,40 +443,14 @@ let configure () =
 
   let cmd_editor = 
     string
-      ~f:(fun s -> 
-	    !current.cmd_editor <- 
-	    try 
-	      let i = String.index s '%' in
-	      let pre = (String.sub s 0 i) in
-	      if String.length s - 1 = i then 
-		pre,""
-	      else
-		let post = String.sub s (i+2) (String.length s - i - 2) in
-		prerr_endline pre;
-		prerr_endline post;
-		pre,post
-	    with Not_found -> s,""
-	    )
+      ~f:(fun s -> !current.cmd_editor <- split_string_format s)
       ~help:"(%s for file name)" 
       "External editor"
       ((fst !current.cmd_editor)^"%s"^(snd !current.cmd_editor))
   in    
   let cmd_browse = 
     string
-      ~f:(fun s -> 
-	    !current.cmd_browse <- 
-	    try 
-	      let i = String.index s '%' in
-	      let pre = (String.sub s 0 i) in
-	      if String.length s - 1 = i then 
-		pre,""
-	      else
-		let post = String.sub s (i+2) (String.length s - i - 2) in
-		prerr_endline pre;
-		prerr_endline post;
-		pre,post
-	    with Not_found -> s,""
-	    )
+      ~f:(fun s -> !current.cmd_browse <- split_string_format s)
       ~help:"(%s for url)" 
       "    Browser"
       ((fst !current.cmd_browse)^"%s"^(snd !current.cmd_browse))
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 048707a3..25535aa4 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: preferences.mli,v 1.8.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
+(*i $Id: preferences.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
 type pref =
     {
diff --git a/ide/undo.ml b/ide/undo.ml
index 6f740667..f617d289 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: undo.ml,v 1.8.2.2 2005/11/16 17:22:39 barras Exp $ *)
+(* $Id: undo.ml 7603 2005-11-23 17:21:53Z barras $ *)
 
 open GText
 open Ideutils
@@ -71,7 +71,6 @@ object(self)
 	      (self#buffer#insert_interactive ~iter s) or
 	      (Stack.push act history; false)
       in if r then begin
-	process_pending ();
 	let act = Stack.pop history in
 	Queue.push act redo;
 	Stack.push act nredo
@@ -107,8 +106,8 @@ object(self)
 		   Queue.iter (fun e -> Stack.push e history) redo;
 		   Queue.clear redo;
 		 end;
-		 let pos = it#offset in
-(*		 if Stack.is_empty history or 
+(*		 let pos = it#offset in
+		 if Stack.is_empty history or 
 		   s=" " or s="\t" or s="\n" or
 					(match Stack.top history with 
 					   | Insert(old,opos,olen) -> 
diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli
index d81d08d5..b87f6559 100644
--- a/ide/undo_lablgtk_ge26.mli
+++ b/ide/undo_lablgtk_ge26.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: undo_lablgtk_ge26.mli,v 1.1.2.1 2005/11/18 16:37:28 herbelin Exp $ i*)
+(*i $Id: undo_lablgtk_ge26.mli 7580 2005-11-18 17:09:10Z herbelin $ i*)
 
 (* An undoable view class *)
 
diff --git a/ide/undo_lablgtk_lt26.mli b/ide/undo_lablgtk_lt26.mli
index 9c2176b0..ddee31d2 100644
--- a/ide/undo_lablgtk_lt26.mli
+++ b/ide/undo_lablgtk_lt26.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: undo_lablgtk_lt26.mli,v 1.1.2.1 2005/11/18 16:37:28 herbelin Exp $ i*)
+(*i $Id: undo_lablgtk_lt26.mli 7580 2005-11-18 17:09:10Z herbelin $ i*)
 
 (* An undoable view class *)
 
diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll
index 4c88adc5..7e6484e1 100644
--- a/ide/utf8_convert.mll
+++ b/ide/utf8_convert.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: utf8_convert.mll,v 1.1.2.1 2004/07/16 19:30:21 herbelin Exp $ *)
+(* $Id: utf8_convert.mll 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 {
   open Lexing 
diff --git a/ide/utils/config_file.ml b/ide/utils/config_file.ml
new file mode 100644
index 00000000..30eb0111
--- /dev/null
+++ b/ide/utils/config_file.ml
@@ -0,0 +1,642 @@
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
+
+(* $Id: config_file.ml 8618 2006-03-08 11:44:47Z notin $ *)
+
+(* TODO *)
+(* section comments *)
+(* better obsoletes: no "{}", line cuts *)
+
+(* possible improvements: *)
+(* use lex/yacc instead of genlex to be more robust, efficient, allow arrays and other types, read comments. *)
+(* description and help, level (beginner/advanced/...) for each cp *)
+(* find an option from its name and group *)
+(* class hooks *)
+(* get the sections of a group / of a file *)
+(* read file format from inifiles and ConfigParser *)
+
+
+(* Read the mli before reading this file! *)
+
+
+(* ******************************************************************************** *)
+(* ******************************** misc utilities ******************************** *)
+(* ******************************************************************************** *)
+(* This code is intended to be usable without any dependencies. *)
+
+(* pipeline style, see for instance Raw.of_channel. *)
+let (|>) x f  = f x
+
+(* as List.assoc, but applies f to the element matching [key] and returns the list
+where this element has been replaced by the result of f. *)
+let rec list_assoc_remove key f = function
+  | [] -> raise Not_found
+  | (key',value) as elt :: tail ->
+      if key <> key'
+      then elt :: list_assoc_remove key f tail
+      else match f value with
+        | None -> tail
+        | Some a -> (key',a) :: tail
+
+(* reminiscent of String.concat. Same as [Queue.iter f1 queue]
+   but calls [f2 ()] between each calls to f1.
+   Does not call f2 before the first call nor after the last call to f2.
+   Could be more efficient with a richer module interface of Queue.
+*)
+let queue_iter_between f1 f2 queue =
+(*   let f flag elt = if flag then f2 (); (f1 elt:unit); true in *)
+  let f flag elt = if flag then f2 (); f1 elt; true in
+  ignore (Queue.fold f false queue)
+
+let list_iter_between f1 f2 = function
+    [] -> ()
+  | a::[] -> f1 a
+  | a::tail -> f1 a; List.iter (fun elt -> (f2 ():unit); f1 elt) tail
+(*   | a::tail -> f1 a; List.iter (fun elt -> f2 (); f1 elt) tail *)
+(* !! types ??? *)
+
+(* to ensure that strings will be parsed correctly by Genlex.
+It's more comfortable not to have quotes around the string, but sometimes it's necessary. *)
+exception Unsafe_string
+let safe_string s =
+  if s = ""
+  then "\"\""
+  else if (
+    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 Unsafe_string
+          done;
+        false
+      | _ ->
+          try
+            string_of_int (int_of_string s) <> s ||
+            string_of_float (float_of_string s) <> s
+          with Failure "int_of_string" | Failure "float_of_string" -> true
+    with Unsafe_string -> true)
+  then Printf.sprintf "\"%s\"" (String.escaped s)
+  else s
+
+
+(* ******************************************************************************** *)
+(* ************************************* core ************************************* *)
+(* ******************************************************************************** *)
+
+module Raw = struct
+  type cp =
+    | String of string
+    | Int of int
+    | Float of float
+    | List of cp list
+    | Tuple of cp list
+    | Section of (string * cp) list
+
+(* code generated by
+camlp4 pa_o.cmo pa_op.cmo pr_o.cmo -- -o config_file_parser.ml -impl config_file_parser.ml4
+Unreadable on purpose, edit the file config_file_parser.ml4 rather than editing this (huge) lines. Then manually copy-paste here the content of config_file_parser.ml.
+Could be one day rewritten with ocamllex/yacc to be more robust, efficient, allow arrays, read comments...*)
+  module Parse = struct
+    let lexer = Genlex.make_lexer ["="; "{"; "}"; "["; "]"; ";"; "("; ")"; ","]
+    let rec file l (strm__ : _ Stream.t) = match try Some (ident strm__) with Stream.Failure -> None with Some id -> begin match Stream.peek strm__ with Some (Genlex.Kwd "=") -> Stream.junk strm__; let v = try value strm__ with Stream.Failure -> raise (Stream.Error "") in begin try file ((id, v) :: l) strm__ with Stream.Failure -> raise (Stream.Error "") end | _ -> raise (Stream.Error "") end | _ -> List.rev l
+    and value (strm__ : _ Stream.t) = match Stream.peek strm__ with Some (Genlex.Kwd "{") -> Stream.junk strm__; let v = try file [] strm__ with Stream.Failure -> raise (Stream.Error "") in begin match Stream.peek strm__ with Some (Genlex.Kwd "}") -> Stream.junk strm__; Section v | _ -> raise (Stream.Error "") end | Some (Genlex.Ident s) -> Stream.junk strm__; String s | Some (Genlex.String s) -> Stream.junk strm__; String s | Some (Genlex.Int i) -> Stream.junk strm__; Int i | Some (Genlex.Float f) -> Stream.junk strm__; Float f | Some (Genlex.Char c) -> Stream.junk strm__; String (String.make 1 c) | Some (Genlex.Kwd "[") -> Stream.junk strm__; let v = try list [] strm__ with Stream.Failure -> raise (Stream.Error "") in List v | Some (Genlex.Kwd "(") -> Stream.junk strm__; let v = try list [] strm__ with Stream.Failure -> raise (Stream.Error "") in Tuple v | _ -> raise Stream.Failure
+    and ident (strm__ : _ Stream.t) = match Stream.peek strm__ with Some (Genlex.Ident s) -> Stream.junk strm__; s | Some (Genlex.String s) -> Stream.junk strm__; s | _ -> raise Stream.Failure
+    and list l (strm__ : _ Stream.t) = match Stream.peek strm__ with Some (Genlex.Kwd ";") -> Stream.junk strm__; begin try list l strm__ with Stream.Failure -> raise (Stream.Error "") end | Some (Genlex.Kwd ",") -> Stream.junk strm__; begin try list l strm__ with Stream.Failure -> raise (Stream.Error "") end | _ -> match try Some (value strm__) with Stream.Failure -> None with Some v -> begin try list (v :: l) strm__ with Stream.Failure -> raise (Stream.Error "") end | _ -> match Stream.peek strm__ with Some (Genlex.Kwd "]") -> Stream.junk strm__; List.rev l | Some (Genlex.Kwd ")") -> Stream.junk strm__; List.rev l | _ -> raise Stream.Failure
+  end
+
+  open Format
+  (* formating convention: the caller has to open the box, close it and flush the output *)
+  (* remarks on Format:
+     set_margin impose un appel à set_max_indent
+     sprintf et bprintf sont flushées à chaque appel*)
+
+  (* pretty print a Raw.cp *)
+  let rec save formatter = function
+    | String s -> fprintf formatter "%s" (safe_string s) (* How can I cut lines and *)
+    | Int i -> fprintf formatter "%d" i             (* print backslashes just before the \n? *)
+    | Float f -> fprintf formatter "%g" f
+    | List l ->
+        fprintf formatter "[@[<b0>";
+        list_iter_between
+          (fun v -> fprintf formatter "@[<b2>"; save formatter v; fprintf formatter "@]")
+          (fun () -> fprintf formatter ";@ ")
+          l;
+        fprintf formatter "@]]"
+    | Tuple l ->
+        fprintf formatter "(@[<b0>";
+        list_iter_between
+          (fun v -> fprintf formatter "@[<b2>"; save formatter v; fprintf formatter "@]")
+          (fun () -> fprintf formatter ",@ ")
+          l;
+        fprintf formatter "@])"
+    | Section l ->
+        fprintf formatter "{@;<0 2>@[<hv0>";
+        list_iter_between
+          (fun (name,value) ->
+             fprintf formatter "@[<hov2>%s =@ @[<b2>" name;
+             save formatter value;
+             fprintf formatter "@]@]";)
+          (fun () -> fprintf formatter "@;<2 0>")
+          l;
+        fprintf formatter "@]}"
+
+(*   let to_string r = save str_formatter r; flush_str_formatter () *)
+  let to_channel out_channel r =
+    let f = formatter_of_out_channel out_channel in
+    fprintf f "@[<b2>"; save f r; fprintf f "@]@?"
+
+  let of_string s = s |> Stream.of_string |> Parse.lexer |> Parse.value
+
+  let of_channel in_channel =
+    let result = in_channel |> Stream.of_channel |> Parse.lexer |> Parse.file [] in
+    close_in in_channel;
+    result
+end
+
+(* print the given string in a way compatible with Format.
+   Truncate the lines when needed, indent the newlines.*)
+let print_help formatter =
+  String.iter (function
+   | ' ' -> Format.pp_print_space formatter ()
+   | '\n' -> Format.pp_force_newline formatter ()
+   | c -> Format.pp_print_char formatter c)
+
+type 'a wrappers = {
+ to_raw : 'a -> Raw.cp;
+ of_raw : Raw.cp -> 'a}
+
+class type ['a] cp = object
+(*   method private to_raw = wrappers.to_raw *)
+(*   method private of_raw = wrappers.of_raw *)
+(*   method private set_string s = s |> Raw.of_string |> self#of_raw |> self#set *)
+  method add_hook : ('a -> 'a -> unit) -> unit
+  method get : 'a
+  method get_default : 'a
+  method set : 'a -> unit
+  method reset : unit
+
+  method get_formatted : Format.formatter -> unit
+  method get_default_formatted : Format.formatter -> unit
+  method get_help_formatted : Format.formatter -> unit
+
+  method get_name : string list
+  method get_short_name : string option
+  method set_short_name : string -> unit
+  method get_help : string
+  method get_spec : Arg.spec
+
+  method set_raw : Raw.cp -> unit
+end
+
+type groupable_cp = <
+  get_name : string list;
+  get_short_name : string option;
+  get_help : string;
+
+  get_formatted : Format.formatter -> unit;
+  get_default_formatted : Format.formatter -> unit;
+  get_help_formatted : Format.formatter -> unit;
+  get_spec : Arg.spec;
+
+  reset : unit;
+  set_raw : Raw.cp -> unit; >
+
+exception Double_name
+exception Missing_cp of groupable_cp
+exception Wrong_type of (out_channel -> unit)
+
+(* Two exceptions to stop the iteration on queues. *)
+exception Found
+exception Found_cp of groupable_cp
+
+(* The data structure to store the cps.
+It's a tree, each node is a section, and a queue of sons with their name.
+Each leaf contains a cp. *)
+type 'a nametree =
+  | Immediate of 'a
+  | Subsection of ((string * 'a nametree) Queue.t)
+      (* this Queue must be nonempty for group.read.choose *)
+
+class group = object (self)
+  val mutable cps = Queue.create () (* hold all the added cps, in a nametree. *)
+
+  method add : 'a. 'a cp -> unit = fun original_cp ->
+    let cp = (original_cp :> groupable_cp) in
+    (* function called when we reach the end of the list cp#get_name. *)
+    let add_immediate name cp queue =
+      Queue.iter (fun (name',_) -> if name = name' then raise Double_name) queue;
+      Queue.push (name, Immediate cp) queue in
+    (* adds the cp with name [first_name::last_name] in section [section]. *)
+    let rec add_in_section section first_name last_name cp queue =
+      let sub_add = match last_name with (* what to do once we have find the correct section *)
+        | [] -> add_immediate first_name
+        | middle_name :: last_name -> add_in_section first_name middle_name last_name in
+      try
+        Queue.iter
+          (function
+             | name, Subsection subsection when name = section ->
+                 sub_add cp subsection; raise Found
+             | _ -> ())
+          queue;
+        let sub_queue = Queue.create () in
+        sub_add cp sub_queue;
+        Queue.push (section, Subsection sub_queue) queue
+      with Found -> () in
+    (match cp#get_name with
+      | [] -> failwith "empty name"
+      | first_name :: [] -> add_immediate first_name cp cps
+      | first_name :: middle_name :: last_name ->
+          add_in_section first_name middle_name last_name cp cps)
+
+  method write ?(with_help=true) filename =
+    let out_channel = open_out filename in
+    let formatter = Format.formatter_of_out_channel out_channel in
+    let print = Format.fprintf formatter in
+    print "@[<v>";
+    let rec save_queue formatter =
+      queue_iter_between
+        (fun (name,nametree) -> save_nametree name nametree)
+        (Format.pp_print_cut formatter)
+    and save_nametree name = function
+      | Immediate cp ->
+          if with_help && cp#get_help <> "" then
+            (print "@[<hov3>(* "; cp#get_help_formatted formatter;
+             print "@ *)@]@,");
+          Format.fprintf formatter "@[<hov2>%s =@ @[<b2>" (safe_string name);
+          cp#get_formatted formatter;
+          print "@]@]"
+      | Subsection queue ->
+          Format.fprintf formatter "%s = {@;<0 2>@[<v>" (safe_string name);
+          save_queue formatter queue;
+          print "@]@,}" in
+    save_queue formatter cps;
+    print "@]@."; close_out out_channel
+
+  method read ?obsoletes ?(no_default=false)
+      ?(on_type_error = fun groupable_cp raw_cp output filename in_channel ->
+          close_in in_channel;
+          Printf.eprintf
+            "Type error while loading configuration parameter %s from file %s.\n%!"
+            (String.concat "." groupable_cp#get_name) filename;
+          output stderr;
+          exit 1)
+      filename =
+    (* [filename] is created if it doesn't exist. In this case there is no need to read it. *)
+    match Sys.file_exists filename with false -> self#write filename | true ->
+    let in_channel = open_in filename in
+    (* what to do when a cp is missing: *)
+    let missing cp default = if no_default then raise (Missing_cp cp) else default in
+    (* returns a cp contained in the nametree queue, which must be nonempty *)
+    let choose queue =
+      let rec iter q = Queue.iter (function
+        | _, Immediate cp -> raise (Found_cp cp)
+        | _, Subsection q -> iter q) q in
+      try iter queue; failwith "choose" with Found_cp cp -> cp in
+    (* [set_and_remove raw_cps nametree] sets the cp of [nametree] to their value
+       defined in [raw_cps] and returns the remaining raw_cps. *)
+    let set_cp cp value =
+      try cp#set_raw value
+      with Wrong_type output -> on_type_error cp value output filename in_channel in
+    let rec set_and_remove raw_cps = function
+      | name, Immediate cp ->
+          (try list_assoc_remove name (fun value -> set_cp cp value; None) raw_cps
+           with Not_found -> missing cp raw_cps)
+      | name, Subsection queue ->
+          (try list_assoc_remove name
+             (function
+                | Raw.Section l ->
+                    (match remainings l queue with
+                       | [] -> None
+                       | l -> Some (Raw.Section l))
+                | r -> missing (choose queue) (Some r))
+             raw_cps
+           with Not_found -> missing (choose queue) raw_cps)
+    and remainings raw_cps queue = Queue.fold set_and_remove raw_cps queue in
+    let remainings = remainings (Raw.of_channel in_channel) cps in
+    (* Handling of cps defined in filename but not belonging to self. *)
+    if remainings <> [] then match obsoletes with
+      | Some filename ->
+          let out_channel =
+            open_out filename in
+(*             open_out_gen [Open_wronly; Open_creat; Open_append; Open_text] 0o666 filename in *)
+          let formatter = Format.formatter_of_out_channel out_channel in
+          Format.fprintf formatter "@[<v>";
+          Raw.save formatter (Raw.Section remainings);
+          Format.fprintf formatter "@]@.";
+          close_out out_channel
+      | None -> ()
+
+  method command_line_args ~section_separator =
+    let print = Format.fprintf Format.str_formatter in (* shortcut *)
+    let result = ref [] in let push x = result := x :: !result in
+    let rec iter = function
+      | _, Immediate cp ->
+          let key = "-" ^ String.concat section_separator cp#get_name in
+          let spec = cp#get_spec in
+          let doc = (
+            print "@[<hv5>";
+            Format.pp_print_as Format.str_formatter (String.length key +3) "";
+            if cp#get_help <> ""
+            then (print "@,@[<b2>"; cp#get_help_formatted Format.str_formatter; print "@]@ ")
+            else print "@,";
+            print "@[<hv>@[current:@;<1 2>@[<hov1>"; cp#get_formatted Format.str_formatter;
+            print "@]@],@ @[default:@;<1 2>@[<b2>"; cp#get_default_formatted Format.str_formatter;
+            print "@]@]@]@]";
+            Format.flush_str_formatter ()) in
+          (match cp#get_short_name with
+            | None -> ()
+            | Some short_name -> push ("-" ^ short_name,spec,""));
+          push (key,spec,doc)
+      | _, Subsection queue -> Queue.iter iter queue in
+    Queue.iter iter cps;
+    List.rev !result
+end
+
+
+(* Given wrappers for the type 'a, cp_custom_type defines a class 'a cp. *)
+class ['a] cp_custom_type wrappers
+  ?group:(group:group option) name ?short_name default help =
+object (self)
+  method private to_raw = wrappers.to_raw
+  method private of_raw = wrappers.of_raw
+
+  val mutable value = default
+    (* output *)
+  method get = value
+  method get_default = default
+  method get_formatted formatter = self#get |> self#to_raw |> Raw.save formatter
+  method get_default_formatted formatter = self#get_default |> self#to_raw |> Raw.save formatter
+    (* input *)
+  method set v = let v' = value in value <- v; self#exec_hooks v' v
+  method set_raw v = self#of_raw v |> self#set
+  method private set_string s = s |> Raw.of_string |> self#of_raw |> self#set
+  method reset = self#set self#get_default
+
+  (* name *)
+  val mutable shortname = short_name
+  method get_name = name
+  method get_short_name = shortname
+  method set_short_name s = shortname <- Some s
+
+  (* help *)
+  method get_help = help
+  method get_help_formatted formatter = print_help formatter self#get_help
+  method get_spec = Arg.String self#set_string
+
+  (* hooks *)
+  val mutable hooks = []
+  method add_hook f = hooks <- (f:'a->'a->unit) :: hooks
+  method private exec_hooks v' v = List.iter (fun f -> f v' v) hooks
+
+  initializer match group with Some g -> g#add (self :> 'a cp) | None -> ()
+end
+
+
+(* ******************************************************************************** *)
+(* ****************************** predefined classes ****************************** *)
+(* ******************************************************************************** *)
+
+let int_wrappers = {
+  to_raw = (fun v -> Raw.Int v);
+  of_raw = function
+    | Raw.Int v -> v
+    | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw.Int expected, got %a\n%!" Raw.to_channel r))}
+class int_cp ?group name ?short_name default help = object (self)
+  inherit [int] cp_custom_type int_wrappers ?group name ?short_name default help
+  method get_spec = Arg.Int self#set
+end
+
+let float_wrappers = {
+  to_raw = (fun v -> Raw.Float v);
+  of_raw = function
+    | Raw.Float v -> v
+    | Raw.Int v -> float v
+    | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw.Float expected, got %a\n%!" Raw.to_channel r))
+}
+class float_cp ?group name ?short_name default help = object (self)
+  inherit [float] cp_custom_type float_wrappers ?group name ?short_name default help
+  method get_spec = Arg.Float self#set
+end
+
+(* The Pervasives version is too restrictive *)
+let bool_of_string s =
+  match String.lowercase s with
+    | "false" | "no" | "n" | "0" -> false (* "0" and "1" aren't used. *)
+    | "true" | "yes" | "y" | "1" -> true
+    | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw.Bool expected, got %s\n%!" r))
+let bool_wrappers = {
+  to_raw = (fun v -> Raw.String (string_of_bool v));
+  of_raw = function
+    | Raw.String v -> bool_of_string v
+    | Raw.Int v -> v <> 0
+    | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw.Bool expected, got %a\n%!" Raw.to_channel r))
+}
+class bool_cp ?group name ?short_name default help = object (self)
+  inherit [bool] cp_custom_type bool_wrappers ?group name ?short_name default help
+  method get_spec = Arg.Bool self#set
+end
+
+let string_wrappers = {
+  to_raw = (fun v -> Raw.String v);
+  of_raw = function
+    | Raw.String v -> v
+    | Raw.Int v -> string_of_int v
+    | Raw.Float v -> string_of_float v
+    | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw.String expected, got %a\n%!" Raw.to_channel r))
+}
+class string_cp ?group name ?short_name default help = object (self)
+  inherit [string] cp_custom_type string_wrappers ?group name ?short_name default help
+  method private of_string s = s
+  method get_spec = Arg.String self#set
+end
+
+let list_wrappers wrappers = {
+  to_raw = (fun l -> Raw.List (List.map wrappers.to_raw l));
+  of_raw = function
+    | Raw.List l -> List.map wrappers.of_raw l
+    | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw.List expected, got %a\n%!" Raw.to_channel r))
+}
+class ['a] list_cp wrappers = ['a list] cp_custom_type (list_wrappers wrappers)
+
+let option_wrappers wrappers = {
+  to_raw = (function
+    | Some v -> wrappers.to_raw v
+    | None -> Raw.String "");
+  of_raw = function
+    | Raw.String s as v -> (
+        if s = "" || s = "None" then None
+        else if String.length s >= 5 && String.sub s 0 5 = "Some "
+        then Some (wrappers.of_raw (Raw.String (String.sub s 5 (String.length s -5))))
+        else Some (wrappers.of_raw v))
+    | r -> Some (wrappers.of_raw r)}
+class ['a] option_cp wrappers = ['a option] cp_custom_type (option_wrappers wrappers)
+
+let enumeration_wrappers enum =
+  let switched = List.map (fun (string,cons) -> cons,string) enum in
+  {to_raw = (fun v -> Raw.String (List.assq v switched));
+   of_raw = function
+     | Raw.String s ->
+         (try List.assoc s enum
+          with Not_found -> failwith (Printf.sprintf "%s isn't a known constructor" s))
+     | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw enumeration expected, got %a\n%!" Raw.to_channel r))
+}
+class ['a] enumeration_cp enum ?group name ?short_name default help = object (self)
+  inherit ['a] cp_custom_type (enumeration_wrappers enum)
+    ?group name ?short_name default help
+  method get_spec = Arg.Symbol (List.map fst enum, (fun s -> self#set (List.assoc s enum)))
+end
+
+let tuple2_wrappers wrapa wrapb = {
+  to_raw = (fun (a,b) -> Raw.Tuple [wrapa.to_raw a; wrapb.to_raw b]);
+  of_raw = function
+    | Raw.Tuple [a;b] -> wrapa.of_raw a, wrapb.of_raw b
+    | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw.Tuple 2 expected, got %a\n%!" Raw.to_channel r))
+}
+class ['a, 'b] tuple2_cp wrapa wrapb = ['a*'b] cp_custom_type (tuple2_wrappers wrapa wrapb)
+
+let tuple3_wrappers wrapa wrapb wrapc = {
+  to_raw = (fun (a,b,c) -> Raw.Tuple[wrapa.to_raw a; wrapb.to_raw b; wrapc.to_raw c]);
+  of_raw = function
+    | Raw.Tuple [a;b;c] -> wrapa.of_raw a, wrapb.of_raw b, wrapc.of_raw c
+    | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw.Tuple 3 expected, got %a\n%!" Raw.to_channel r))
+}
+class ['a,'b,'c] tuple3_cp wrapa wrapb wrapc =
+  ['a*'b*'c] cp_custom_type (tuple3_wrappers wrapa wrapb wrapc)
+
+let tuple4_wrappers wrapa wrapb wrapc wrapd = {
+  to_raw=(fun (a,b,c,d)->Raw.Tuple[wrapa.to_raw a;wrapb.to_raw b;wrapc.to_raw c;wrapd.to_raw d]);
+  of_raw = function
+    | Raw.Tuple [a;b;c;d] -> wrapa.of_raw a, wrapb.of_raw b, wrapc.of_raw c, wrapd.of_raw d
+    | r -> raise (Wrong_type (fun outchan -> Printf.fprintf outchan
+                                "Raw.Tuple 4 expected, got %a\n%!" Raw.to_channel r))
+}
+class ['a,'b,'c,'d] tuple4_cp wrapa wrapb wrapc wrapd =
+  ['a*'b*'c*'d] cp_custom_type (tuple4_wrappers wrapa wrapb wrapc wrapd)
+
+class string2_cp = [string,string] tuple2_cp string_wrappers string_wrappers
+(* class color_cp = string_cp *)
+class font_cp = string_cp
+class filename_cp = string_cp
+
+
+(* ******************************************************************************** *)
+(******************** Backward compatibility with module Options ****************** *)
+(* ******************************************************************************** *)
+
+type 'a option_class = 'a wrappers
+type 'a option_record = 'a cp
+type options_file = {mutable filename:string; group:group}
+
+let create_options_file filename = {filename = filename; group = new group}
+let set_options_file options_file filename = options_file.filename <- filename
+let load {filename=f; group = g} = g#read f
+let append {group=g} filename = g#read filename
+let save {filename=f; group = g} = g#write ~with_help:false f
+let save_with_help {filename=f; group = g} = g#write ~with_help:true f
+let define_option {group=group} name help option_class default =
+  (new cp_custom_type option_class ~group name default help)
+let option_hook cp f = cp#add_hook (fun _ _ -> f ())
+
+let  string_option = string_wrappers
+let   color_option = string_wrappers
+let    font_option = string_wrappers
+let     int_option =    int_wrappers
+let    bool_option =   bool_wrappers
+let   float_option =  float_wrappers
+let string2_option = tuple2_wrappers string_wrappers string_wrappers
+
+let option_option = option_wrappers
+let list_option = list_wrappers
+let sum_option = enumeration_wrappers
+let tuple2_option (a,b) = tuple2_wrappers a b
+let tuple3_option (a,b,c) = tuple3_wrappers a b c
+let tuple4_option (a,b,c,d) = tuple4_wrappers a b c d
+
+let ( !! ) cp = cp#get
+let ( =:= ) cp value = cp#set value
+
+let shortname cp = String.concat ":" cp#get_name
+let get_help cp = cp#get_help
+
+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
+
+let rec value_to_raw = function
+  | Module a -> Raw.Section (List.map (fun (name,value) -> name, value_to_raw value) a)
+  | StringValue a -> Raw.String a
+  | IntValue a -> Raw.Int a
+  | FloatValue a -> Raw.Float a
+  | List a -> Raw.List (List.map value_to_raw a)
+  | SmallList a -> Raw.Tuple (List.map value_to_raw a)
+let rec raw_to_value = function
+  | Raw.String a -> StringValue a
+  | Raw.Int a -> IntValue a
+  | Raw.Float a -> FloatValue a
+  | Raw.List a -> List (List.map raw_to_value a)
+  | Raw.Tuple a -> SmallList (List.map raw_to_value a)
+  | Raw.Section a -> Module (List.map (fun (name,value) -> name, raw_to_value value) a)
+
+let define_option_class _ of_option_value to_option_value =
+  {to_raw = (fun a -> a |> to_option_value |> value_to_raw);
+   of_raw = (fun a -> a |> raw_to_value |> of_option_value)}
+
+let to_value {to_raw = to_raw} a = a |> to_raw |> raw_to_value
+let from_value {of_raw = of_raw} a = a |> value_to_raw |> of_raw
+
+let of_value_w wrappers a = a |> value_to_raw |> wrappers.of_raw
+let to_value_w wrappers a = a |> wrappers.to_raw |> raw_to_value
+(* fancy indentation when finishing this stub code, not good style :-) *)
+let value_to_string : option_value -> string = of_value_w string_option
+let  string_to_value = to_value_w  string_option
+let value_to_int     = of_value_w     int_option
+let     int_to_value = to_value_w     int_option
+let value_to_bool    = of_value_w    bool_option
+let    bool_to_value = to_value_w    bool_option
+let value_to_float   = of_value_w   float_option
+let   float_to_value = to_value_w   float_option
+let value_to_string2 = of_value_w string2_option
+let string2_to_value = to_value_w string2_option
+let value_to_list of_value =
+  let wrapper = define_option_class "" of_value (fun _ -> failwith "value_to_list") in
+  of_value_w (list_option wrapper)
+let list_to_value to_value =
+  let wrapper = define_option_class "" (fun _ -> failwith "value_to_list") to_value in
+  to_value_w (list_option wrapper)
diff --git a/ide/utils/config_file.mli b/ide/utils/config_file.mli
new file mode 100644
index 00000000..b9c77682
--- /dev/null
+++ b/ide/utils/config_file.mli
@@ -0,0 +1,352 @@
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
+
+(**
+  This module implements a mechanism to handle configuration files.
+  A configuration file is defined as a set of [variable = value] lines,
+  where value can be
+    a simple string (types int, string, bool...),
+    a list of values between brackets (lists) or parentheses (tuples),
+    or a set of [variable = value] lines between braces.
+  The configuration file is automatically loaded and saved,
+  and configuration parameters are manipulated inside the program as easily as references.
+
+  Object implementation by Jean-Baptiste Rouquier.
+*)
+
+(** {1:lowlevelinterface Low level interface} *)
+(** Skip this section on a first reading... *)
+
+(** The type of cp freshly parsed from configuration file,
+not yet wrapped in their proper type. *)
+module Raw : sig
+  type cp =
+    | String of string (** base types, reproducing the tokens of Genlex *)
+    | Int of int
+    | Float of float
+    | List of cp list (** compound types *)
+    | Tuple of cp list
+    | Section of (string * cp) list
+
+  (** A parser. *)
+  val of_string : string -> cp
+
+  (** Used to print the values into a log file for instance. *)
+  val to_channel : out_channel -> cp -> unit
+end
+
+(** A type used to specialize polymorphics classes and define new classes.
+  {!Config_file.predefinedwrappers} are provided.
+ *)
+type 'a wrappers = { to_raw : 'a -> Raw.cp; of_raw : Raw.cp -> 'a; }
+
+(** An exception raised by {!Config_file.cp.set_raw}
+  when the argument doesn't have a suitable {!Config_file.Raw.cp} type.
+  The function explains the problem and flush the output.*)
+exception Wrong_type of (out_channel -> unit)
+
+(* (\** {2 Miscellaneous functions} *\) *)
+
+(* val bool_of_string : string -> bool *)
+
+(** {1 High level interface} *)
+(** {2 The two main classes} *)
+
+(** A Configuration Parameter, in short cp, ie
+  a value we can store in and read from a configuration file. *)
+class type ['a] cp = object
+  (** {1 Accessing methods} *)
+
+  method get : 'a
+  method set : 'a -> unit
+  method get_default : 'a
+  method get_help : string
+  method get_name : string list
+
+  (** Resets to the default value. *)
+  method reset : unit
+
+  (** {1 Miscellaneous} *)
+
+  (** All the hooks are executed each time the method set is called,
+    just after setting the new value.*)
+  method add_hook : ('a -> 'a -> unit) -> unit
+
+  (** Used to generate command line arguments in {!Config_file.group.command_line_args} *)
+  method set_short_name : string -> unit
+
+  (** [None] if no optional short_name was provided during object creation
+    and [set_short_name] was never called.*)
+  method get_short_name : string option
+
+  (** {1 Methods for internal use} *)
+
+  method get_formatted : Format.formatter -> unit
+  method get_default_formatted : Format.formatter -> unit
+  method get_help_formatted : Format.formatter -> unit
+
+  method get_spec : Arg.spec
+  method set_raw : Raw.cp -> unit
+end
+
+(** Unification over all possible ['a cp]:
+  contains the main methods of ['a cp] except the methods using the type ['a].
+  A [group] manipulates only [groupable_cp] for homogeneity. *)
+type groupable_cp = <
+  get_name : string list;
+  get_short_name : string option;
+  get_help : string;
+
+  get_formatted : Format.formatter -> unit;
+  get_default_formatted : Format.formatter -> unit;
+  get_help_formatted : Format.formatter -> unit;
+  get_spec : Arg.spec;
+
+  reset : unit;
+  set_raw : Raw.cp -> unit; >
+
+(** Raised in case a name is already used.
+  See {!Config_file.group.add} *)
+exception Double_name
+
+(** An exception possibly raised if we want to check that
+  every cp is defined in a configuration file.
+  See {!Config_file.group.read}.
+*)
+exception Missing_cp of groupable_cp
+
+(** A group of cps, that can be loaded and saved,
+or used to generate command line arguments.
+
+The basic usage is to have only one group and one configuration file,
+but this mechanism allows to have more,
+for instance to have another smaller group for the options to pass on the command line.
+*)
+class group : object
+  (** Adds a cp to the group.
+    Note that the type ['a] must be lost
+    to allow cps of different types to belong to the same group.
+    @raise Double_name if [cp#get_name] is already used. *)
+(*     method add : 'a cp -> 'a cp *)
+    method add : 'a cp -> unit
+
+    (**[write filename] saves all the cps into the configuration file [filename].*)
+    method write : ?with_help:bool -> string -> unit
+
+    (** [read filename] reads [filename]
+      and stores the values it specifies into the cps belonging to this group.
+      The file is created (and not read) if it doesn't exists.
+      In the default behaviour, no warning is issued
+      if not all cps are updated or if some values of [filename] aren't used.
+
+      If [obsoletes] is specified,
+      then prints in this file all the values that are
+      in [filename] but not in this group.
+      Those cps are likely to be erroneous or obsolete.
+      Opens this file only if there is something to write in it.
+
+      If [no_default] is [true], then raises [Missing_cp foo] if
+      the cp [foo] isn't defined in [filename] but belongs to this group.
+
+      [on_type_error groupable_cp value output filename in_channel]
+      is called if the file doesn't give suitable value
+      (string instead of int for instance, or a string not belonging to the expected enumeration)
+      for the cp [groupable_cp].
+      [value] is the value read from the file,
+      [output] is the argument of {!Config_file.Wrong_type},
+      [filename] is the same argument as the one given to read,
+      and [in_channel] refers to [filename] to allow a function to close it if needed.
+      Default behaviour is to print an error message and call [exit 1].
+*)
+    method read : ?obsoletes:string -> ?no_default:bool ->
+      ?on_type_error : (groupable_cp -> Raw.cp -> (out_channel -> unit) ->
+                          string -> in_channel -> unit) ->
+      string -> unit
+
+    (** Interface with module Arg.
+      @param section_separator the string used to concatenate the name of a cp,
+      to get the command line option name.
+      ["-"] is a good default.
+      @return a list that can be used with [Arg.parse] and [Arg.usage].*)
+    method command_line_args : section_separator:string -> (string * Arg.spec * string) list
+  end
+
+(** {2 Predefined cp classes} *)
+
+(** The last three non-optional arguments are always
+  [name] (of type string list), [default_value] and [help] (of type string).
+
+  [name] is the path to the cp: [["section";"subsection"; ...; "foo"]].
+  It can consists of a single element but must not be empty.
+
+  [short_name] will be added a "-" and used in
+  {!Config_file.group.command_line_args}.
+
+  [group], if provided, adds the freshly defined option to it
+  (something like [initializer group#add self]).
+
+  [help] needs not contain newlines, it will be automatically truncated where needed.
+  It is mandatory but can be [""].
+*)
+
+class int_cp : ?group:group -> string list -> ?short_name:string -> int -> string -> [int] cp
+class float_cp : ?group:group -> string list -> ?short_name:string -> float -> string -> [float] cp
+class bool_cp : ?group:group -> string list -> ?short_name:string -> bool -> string -> [bool] cp
+class string_cp : ?group:group -> string list -> ?short_name:string -> string -> string -> [string] cp
+class ['a] list_cp : 'a wrappers -> ?group:group -> string list -> ?short_name:string -> 'a list -> string -> ['a list] cp
+class ['a] option_cp : 'a wrappers -> ?group:group -> string list -> ?short_name:string -> 'a option -> string -> ['a option] cp
+class ['a] enumeration_cp : (string * 'a) list -> ?group:group -> string list -> ?short_name:string -> 'a -> string -> ['a] cp
+class ['a, 'b] tuple2_cp : 'a wrappers -> 'b wrappers -> ?group:group -> string list -> ?short_name:string -> 'a * 'b -> string -> ['a * 'b] cp
+class ['a, 'b, 'c] tuple3_cp : 'a wrappers -> 'b wrappers -> 'c wrappers -> ?group:group -> string list -> ?short_name:string -> 'a * 'b * 'c -> string -> ['a * 'b * 'c] cp
+class ['a, 'b, 'c, 'd] tuple4_cp : 'a wrappers -> 'b wrappers -> 'c wrappers -> 'd wrappers -> ?group:group -> string list -> ?short_name:string -> 'a * 'b * 'c * 'd -> string -> ['a * 'b * 'c * 'd] cp
+class string2_cp : ?group:group -> string list -> ?short_name:string -> string * string -> string -> [string, string] tuple2_cp
+(* class color_cp : ?group:group -> string list -> ?short_name:string -> string -> string -> string_cp *)
+class font_cp : ?group:group -> string list -> ?short_name:string -> string -> string -> string_cp
+class filename_cp : ?group:group -> string list -> ?short_name:string -> string -> string -> string_cp
+
+(** {2:predefinedwrappers Predefined wrappers} *)
+
+val int_wrappers : int wrappers
+val float_wrappers : float wrappers
+val bool_wrappers : bool wrappers
+val string_wrappers : string wrappers
+val list_wrappers : 'a wrappers -> 'a list wrappers
+val option_wrappers : 'a wrappers -> 'a option wrappers
+
+(** If you have a [type suit = Spades | Hearts | Diamond | Clubs], then
+{[enumeration_wrappers ["spades",Spades; "hearts",Hearts; "diamond",Diamond; "clubs",Clubs]]}
+will allow you to use cp of this type.
+For sum types with not only constant constructors,
+you will need to define your own cp class. *)
+val enumeration_wrappers : (string * 'a) list -> 'a wrappers
+val tuple2_wrappers : 'a wrappers -> 'b wrappers -> ('a * 'b) wrappers
+val tuple3_wrappers : 'a wrappers -> 'b wrappers -> 'c wrappers -> ('a * 'b * 'c) wrappers
+val tuple4_wrappers : 'a wrappers -> 'b wrappers -> 'c wrappers -> 'd wrappers -> ('a * 'b * 'c * 'd) wrappers
+
+(** {2 Defining new cp classes} *)
+
+(** To define a new cp class, you just have to provide an implementation for the wrappers
+between your type [foo] and the type [Raw.cp].
+Once you have your wrappers [w], write
+{[class foo_cp = [foo] cp_custom_type w]}
+
+For further details, have a look at the commented .ml file,
+section "predefined cp classes".
+*)
+class ['a] cp_custom_type : 'a wrappers ->
+  ?group:group -> string list -> ?short_name:string -> 'a -> string -> ['a] cp
+
+
+(** {1 Backward compatibility}
+
+Deprecated.
+
+All the functions from the module Options are available, except:
+
+- [prune_file]: use [group#write ?obsoletes:"foo.ml"].
+- [smalllist_to_value], [smalllist_option]: use lists or tuples.
+- [get_class].
+- [class_hook]: hooks are local to a cp.
+  If you want hooks global to a class,
+  define a new class that inherit from {!Config_file.cp_custom_type}.
+- [set_simple_option], [get_simple_option], [simple_options], [simple_args]:
+  use {!Config_file.group.write}.
+- [set_option_hook]: use {!Config_file.cp.add_hook}.
+- [set_string_wrappers]: define a new class with {!Config_file.cp_custom_type}.
+
+The old configurations files are readable by this module.
+*)
+
+
+
+
+
+(**/**)
+type 'a option_class
+type 'a option_record
+type options_file
+
+val create_options_file : string -> options_file
+val set_options_file : options_file -> string -> unit
+val load : options_file -> unit
+val append : options_file -> string -> unit
+val save : options_file -> unit
+val save_with_help : options_file -> unit
+(* 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
+
+val option_option : 'a option_class -> 'a option option_class
+val list_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
+
+val ( !! ) : 'a option_record -> 'a
+val ( =:= ) : 'a option_record -> 'a -> unit
+val shortname : 'a option_record -> string
+val get_help : 'a option_record -> string
+
+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
diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml
index de6a7c57..275d8616 100644
--- a/ide/utils/configwin.ml
+++ b/ide/utils/configwin.ml
@@ -1,26 +1,27 @@
-(**************************************************************************)
-(*                   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                                *)
-(**************************************************************************)
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
 
 type parameter_kind = Configwin_types.parameter_kind
 
@@ -35,10 +36,16 @@ type return_button =
   | Return_ok
   | Return_cancel
 
-module KeyOption = Configwin_types.KeyOption
+let string_to_key = Configwin_types.string_to_key
+let key_to_string = Configwin_types.key_to_string
+let key_cp_wrapper = Configwin_types.key_cp_wrapper
+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
@@ -53,20 +60,20 @@ let hotkey = Configwin_ihm.hotkey
 let modifiers = Configwin_ihm.modifiers
 let html = Configwin_ihm.html
 
-let edit 
+let edit
     ?(apply=(fun () -> ()))
-    title ?(width=400) ?(height=400) 
-    conf_struct_list = 
+    title ?(width=400) ?(height=400)
+    conf_struct_list =
   Configwin_ihm.edit ~with_apply: true ~apply title ~width ~height conf_struct_list
 
 let get = Configwin_ihm.edit ~with_apply: false ~apply: (fun () -> ())
 
-let simple_edit 
+let simple_edit
     ?(apply=(fun () -> ()))
-    title ?width ?height 
+    title ?width ?height
     param_list = Configwin_ihm.simple_edit ~with_apply: true ~apply title ?width ?height param_list
 
-let simple_get = Configwin_ihm.simple_edit 
+let simple_get = Configwin_ihm.simple_edit
     ~with_apply: false ~apply: (fun () -> ())
 
 let box = Configwin_ihm.box
diff --git a/ide/utils/configwin.mli b/ide/utils/configwin.mli
index 078befc6..2d4dd4a7 100644
--- a/ide/utils/configwin.mli
+++ b/ide/utils/configwin.mli
@@ -1,26 +1,27 @@
-(**************************************************************************)
-(*                   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                                *)
-(**************************************************************************)
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
 
 (** This module is the interface of the Configwin library. *)
 
@@ -30,8 +31,8 @@
 type parameter_kind;;
 
 (** This type represents the structure of the configuration window. *)
-type configuration_structure = 
-  | Section of string * parameter_kind list 
+type configuration_structure =
+  | Section of string * parameter_kind list
        (** label of the section, parameters *)
   | Section_list of string * configuration_structure list
        (** label of the section, list of the sub sections *)
@@ -50,13 +51,20 @@ type return_button =
 	 on the apply button.*)
 
 
-(** {2 The key option class (to use with the {!Uoptions} library)} *)
+(** {2 The key option class (to use with the {!Config_file} library)} *)
 
-module KeyOption : sig
-  val string_to_key : string -> (Gdk.Tags.modifier list * int) 
-  val key_to_string : (Gdk.Tags.modifier list * int) -> string
-  val t : (Gdk.Tags.modifier list * int) Uoptions.option_class
-end
+val string_to_key : string -> Gdk.Tags.modifier list * int
+
+val key_to_string : Gdk.Tags.modifier list * int -> string
+
+val key_cp_wrapper : (Gdk.Tags.modifier list * int) Config_file.wrappers
+
+class key_cp :
+  ?group:Config_file.group ->
+  string list ->
+  ?short_name:string ->
+  Gdk.Tags.modifier list * int ->
+  string -> [Gdk.Tags.modifier list * int] Config_file.cp_custom_type
 
 (** {2 Functions to create parameters} *)
 
@@ -69,6 +77,13 @@ end
 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.
@@ -88,12 +103,12 @@ val bool : ?editable: bool -> ?help: string ->
    always returning false.
 *)
 val strings : ?editable: bool -> ?help: string ->
-  ?f: (string list -> unit) -> 
+  ?f: (string list -> unit) ->
     ?eq: (string -> string -> bool) ->
-      ?add: (unit -> string list) -> 
+      ?add: (unit -> string list) ->
 	string -> string list -> parameter_kind
-	
-(** [list label f_strings value] creates a list parameter. 
+
+(** [list label f_strings value] creates a list parameter.
    [f_strings] is a function taking a value and returning a list
    of strings to display it. The list length should be the same for
    any value, and the same as the titles list length. The [value]
@@ -117,15 +132,15 @@ val strings : ?editable: bool -> ?help: string ->
    no color for any element.
 *)
 val list : ?editable: bool -> ?help: string ->
-  ?f: ('a list -> unit) -> 
+  ?f: ('a list -> unit) ->
     ?eq: ('a -> 'a -> bool) ->
       ?edit: ('a -> 'a) ->
-	?add: (unit -> 'a list) -> 
+	?add: (unit -> 'a list) ->
 	  ?titles: string list ->
 	    ?color: ('a -> string option) ->
-	      string -> 
+	      string ->
 		('a -> string list) ->
-		  'a list -> 
+		  'a list ->
 		    parameter_kind
 
 (** [color label value] creates a color parameter.
@@ -134,7 +149,7 @@ val list : ?editable: bool -> ?help: string ->
    @param help an optional help message.
    @param f the function called to apply the value (default function does nothing).
 *)
-val color : ?editable: bool -> ?expand: bool -> ?help: string -> 
+val color : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (string -> unit) -> string -> string -> parameter_kind
 
 (** [font label value] creates a font parameter.
@@ -143,7 +158,7 @@ val color : ?editable: bool -> ?expand: bool -> ?help: string ->
    @param help an optional help message.
    @param f the function called to apply the value (default function does nothing).
 *)
-val font : ?editable: bool -> ?expand: bool -> ?help: string -> 
+val font : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (string -> unit) -> string -> string -> parameter_kind
 
 (** [combo label choices value] creates a combo parameter.
@@ -156,8 +171,8 @@ val font : ?editable: bool -> ?expand: bool -> ?help: string ->
    @param blank_allowed indicate if the empty selection [""] is accepted
    (default is [false]).
 *)
-val combo : ?editable: bool -> ?expand: bool -> ?help: string -> 
-  ?f: (string -> unit) -> 
+val combo : ?editable: bool -> ?expand: bool -> ?help: string ->
+  ?f: (string -> unit) ->
     ?new_allowed: bool -> ?blank_allowed: bool ->
       string -> string list -> string -> parameter_kind
 
@@ -167,14 +182,21 @@ val combo : ?editable: bool -> ?expand: bool -> ?help: string ->
    @param help an optional help message.
    @param f the function called to apply the value (default function does nothing).
 *)
-val text : ?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 html bindings are available 
-   in the text widget. Use the [configwin_html_config] utility 
+(** 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.
 *)
-val html : ?editable: bool -> ?expand: bool -> ?help: string -> 
+val html : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (string -> unit) -> string -> string -> parameter_kind
 
 (** [filename label value] creates a filename parameter.
@@ -194,8 +216,8 @@ val filename : ?editable: bool -> ?expand: bool -> ?help: string ->
    is [Pervasives.(=)]. If you want to allow doubles in the list, give a function
    always returning false.
 *)
-val filenames : ?editable: bool -> ?help: string -> 
-  ?f: (string list -> unit) -> 
+val filenames : ?editable: bool -> ?help: string ->
+  ?f: (string list -> unit) ->
     ?eq: (string -> string -> bool) ->
       string -> string list -> parameter_kind
 
@@ -208,8 +230,8 @@ val filenames : ?editable: bool -> ?help: string ->
    is a tupe [(day,month,year)], where [month] is between [0] and [11]. The default
    function creates the string [year/month/day].
 *)
-val date : ?editable: bool -> ?expand: bool -> ?help: string -> 
-  ?f: ((int * int * int) -> unit) -> 
+val date : ?editable: bool -> ?expand: bool -> ?help: string ->
+  ?f: ((int * int * int) -> unit) ->
     ?f_string: ((int * int * int -> string)) ->
       string -> (int * int * int) -> parameter_kind
 
@@ -221,7 +243,7 @@ val date : ?editable: bool -> ?expand: bool -> ?help: string ->
    @param f the function called to apply the value (default function does nothing).
 *)
 val hotkey : ?editable: bool -> ?expand: bool -> ?help: string ->
-  ?f: ((Gdk.Tags.modifier list * int) -> unit) -> 
+  ?f: ((Gdk.Tags.modifier list * int) -> unit) ->
     string -> (Gdk.Tags.modifier list * int) -> parameter_kind
 
 val modifiers : ?editable: bool -> ?expand: bool -> ?help: string ->
@@ -229,7 +251,6 @@ val modifiers : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (Gdk.Tags.modifier list -> unit) -> 
     string -> Gdk.Tags.modifier list -> parameter_kind
 
-
 (** [custom box f expand] creates a custom parameter, with
    the given [box], the [f] function is called when the user
    wants to apply his changes, and [expand] indicates if the box
@@ -241,8 +262,8 @@ val custom : ?label: string -> GPack.box -> (unit -> unit) -> bool -> parameter_
 (** {2 Functions creating configuration windows and boxes} *)
 
 (** This function takes a configuration structure and creates a window
-   to configure the various parameters. 
-   @param apply this function is called when the apply button is clicked, after 
+   to configure the various parameters.
+   @param apply this function is called when the apply button is clicked, after
    giving new values to parameters.
 *)
 val edit :
@@ -263,9 +284,9 @@ val get :
   configuration_structure list ->
   return_button
 
-(** This function takes a list of parameter specifications and 
+(** This function takes a list of parameter specifications and
    creates a window to configure the various parameters.
-   @param apply this function is called when the apply button is clicked, after 
+   @param apply this function is called when the apply button is clicked, after
    giving new values to parameters.*)
 val simple_edit :
   ?apply: (unit -> unit) ->
@@ -274,7 +295,7 @@ val simple_edit :
   ?height:int ->
   parameter_kind list -> return_button
 
-(** This function takes a list of parameter specifications and 
+(** This function takes a list of parameter specifications and
    creates a window to configure the various parameters,
    without Apply button.*)
 val simple_get :
@@ -284,17 +305,14 @@ val simple_get :
   parameter_kind list -> return_button
 
 (** Create a [GPack.box] with the list of given parameters,
-   and the given list of buttons (defined by their label and callback).
-   Before calling the callback of a button, the [apply] function
-   of each parameter is called.
+   Return the box and the function to call to apply new values to parameters.
 *)
-val box : parameter_kind list -> 
-  (string * (unit -> unit)) list -> GPack.box
+val box : parameter_kind list -> GData.tooltips -> GPack.box * (unit -> unit)
 
 (** Create a [GPack.box] with the list of given configuration structure list,
    and the given list of buttons (defined by their label and callback).
    Before calling the callback of a button, the [apply] function
    of each parameter is called.
 *)
-val tabbed_box : configuration_structure list -> 
-  (string * (unit -> unit)) list -> GPack.box
+val tabbed_box : configuration_structure list ->
+  (string * (unit -> unit)) list -> GData.tooltips -> GPack.box
diff --git a/ide/utils/configwin_html_config.ml b/ide/utils/configwin_html_config.ml
index fc2913d1..fe39de0a 100644
--- a/ide/utils/configwin_html_config.ml
+++ b/ide/utils/configwin_html_config.ml
@@ -1,38 +1,39 @@
-(**************************************************************************)
-(*                   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                                *)
-(**************************************************************************)
+(*********************************************************************************)
+(*                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 Uoptions
+open Config_file
 
-let simple_get = C.simple_edit 
+let simple_get = C.simple_edit
     ~with_apply: false ~apply: (fun () -> ())
 
 let params_hb hb =
-  let p_key = C.hotkey 
+  let p_key = C.hotkey
       ~f: (fun k -> hb.html_key <- k) Configwin_messages.mKey
       hb.html_key
   in
@@ -53,10 +54,10 @@ let edit_hb hb =
   hb
 
 let add () =
-  let hb = { html_key = KeyOption.string_to_key "C-a" ;
+  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]
@@ -66,18 +67,18 @@ let main () =
   ignore (GMain.Main.init ());
   let (ini, bindings) = C.html_config_file_and_option () in
   let param = C.list
-      ~f: (fun l -> bindings =:= l ; Uoptions.save_with_help ini)
+      ~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 -> [ KeyOption.key_to_string hb.html_key ;
+      (fun hb -> [ Configwin_types.key_to_string hb.html_key ;
 		   hb.html_begin ; hb.html_end ])
-      !!bindings
+      bindings#get
   in
-  ignore (simple_get ~width: 300 ~height: 400 
+  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 03ca706c..e9ba9789 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1,68 +1,73 @@
-(**************************************************************************)
-(*                   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 contains the gui functions of Confgiwin.*)
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
+
+(** This module contains the gui functions of Configwin.*)
 
 open Configwin_types
 
-module O = Uoptions
+module O = Config_file
 
-
-(** The file where the html config is. *)
 let file_html_config = Filename.concat Configwin_messages.home ".configwin_html"
-  
-(** Return the ini file for the html config, and the option for bindings. *)
+
+let debug = false
+let dbg = if debug then prerr_endline else (fun _ -> ())
+
+(** Return the config group for the html config file,
+   and the option for bindings. *)
 let html_config_file_and_option () =
-  let ini = O.create_options_file file_html_config in
-  let bindings = O.define_option ini ["bindings"]
-      ""
-      (O.list_option Configwin_types.Html_binding.t)
-      [ { html_key = KeyOption.string_to_key "A-b" ;
+  let ini = new O.group in
+  let bindings = new O.list_cp
+      Configwin_types.htmlbinding_cp_wrapper
+      ~group: ini
+      ["bindings"]
+      ~short_name: "bd"
+      [ { html_key = Configwin_types.string_to_key "A-b" ;
 	  html_begin = "<b>";
 	  html_end = "</b>" ;
 	} ;
-	{ html_key = KeyOption.string_to_key "A-i" ;
+	{ html_key = Configwin_types.string_to_key "A-i" ;
 	  html_begin = "<i>";
 	  html_end = "</i>" ;
-	} 
-      ]	
+	}
+      ]
+      ""
   in
-  O.load ini ;
+  ini#read file_html_config ;
   (ini, bindings)
 
-
 (** This variable contains the last directory where the user selected a file.*)
 let last_dir = ref "";;
 
 (** This function allows the user to select a file and returns the
-   selected file name. An optional function allows to change the 
+   selected file name. An optional function allows to change the
    behaviour of the ok button.
    A VOIR : mutli-selection ? *)
 let select_files ?dir
     ?(fok : (string -> unit) option)
     the_title =
-  let files = ref ([] : string list) in 
+  let files = ref ([] : string list) in
   let fs = GWindow.file_selection ~modal:true
       ~title: the_title () in
   (* we set the previous directory, if no directory is given *)
@@ -78,7 +83,7 @@ let select_files ?dir
       let _ = fs#set_filename !last_dir in
       ()
   );
- 
+
   let _ = fs # connect#destroy ~callback: GMain.Main.quit in
   let _ = fs # ok_button # connect#clicked ~callback:
       (match fok with
@@ -134,52 +139,55 @@ let select_date title (day,mon,year) =
    one to add items and one to remove the selected items.
    The class takes in parameter a function used to add items and
    a string list ref which is used to store the content of the clist.
-   At last, a title for the frame  is also in parameter, so that     
+   At last, a title for the frame  is also in parameter, so that
    each instance of the class creates a frame. *)
-class ['a] list_selection_box (listref : 'a list ref) 
+class ['a] list_selection_box
+    (listref : 'a list ref)
     titles_opt
     help_opt
     f_edit_opt
     f_strings
     f_color
     (eq : 'a -> 'a -> bool)
-    add_function title editable =
+    add_function title editable
+    (tt:GData.tooltips)
+    =
+  let _ = dbg "list_selection_box" in
   let wev = GBin.event_box () in
   let wf = GBin.frame ~label: title ~packing: wev#add () in
   let hbox = GPack.hbox ~packing: wf#add () in
   (* the scroll window and the clist *)
   let wscroll = GBin.scrolled_window
-      	~vpolicy: `AUTOMATIC
-	~hpolicy: `AUTOMATIC
-      ~packing: (hbox#pack ~expand: true) () 
+      ~vpolicy: `AUTOMATIC
+      ~hpolicy: `AUTOMATIC
+      ~packing: (hbox#pack ~expand: true) ()
   in
   let wlist = match titles_opt with
-    None -> 
+    None ->
       GList.clist ~selection_mode: `MULTIPLE
 	~titles_show: false
 	~packing: wscroll#add ()
-  | Some l -> 
-      GList.clist ~selection_mode: `MULTIPLE 
+  | Some l ->
+      GList.clist ~selection_mode: `MULTIPLE
 	~titles: l
 	~titles_show: true
 	~packing: wscroll#add ()
   in
-  let _ = 
+  let _ =
     match help_opt with
       None -> ()
     | Some help ->
-	let tooltips = GData.tooltips () in
-	ignore (wf#connect#destroy ~callback: tooltips#destroy);
-	tooltips#set_tip wev#coerce ~text: help ~privat: help 
+	tt#set_tip ~text: help ~privat: help wev#coerce
   in  (* the vbox for the buttons *)
   let vbox_buttons = GPack.vbox () in
-  let _ = 
+  let _ =
     if editable then
       let _ = hbox#pack ~expand: false vbox_buttons#coerce in
       ()
     else
-      () 
+      ()
   in
+  let _ = dbg "list_selection_box: wb_add" in
   let wb_add = GButton.button
       ~label: Configwin_messages.mAdd
       ~packing: (vbox_buttons#pack ~expand:false ~padding:2)
@@ -203,6 +211,7 @@ class ['a] list_selection_box (listref : 'a list ref)
       ~packing: (vbox_buttons#pack ~expand:false ~padding:2)
       ()
   in
+  let _ = dbg "list_selection_box: object(self)" in
   object (self)
     (** the list of selected rows *)
     val mutable list_select = []
@@ -216,17 +225,17 @@ class ['a] list_selection_box (listref : 'a list ref)
       (* insert the elements in the clist *)
       wlist#freeze ();
       wlist#clear ();
-      List.iter 
-	(fun ele -> 
+      List.iter
+	(fun ele ->
 	  ignore (wlist#append (f_strings ele));
 	  match f_color ele with
 	    None -> ()
 	  | Some c ->
 	      try wlist#set_row ~foreground: (`NAME c) (wlist#rows - 1)
 	      with _ -> ()
-	) 
+	)
 	!listref;
-      
+
       (match titles_opt with
 	None -> wlist#columns_autosize ()
       |	Some _ -> GToolbox.autosize_clist wlist);
@@ -280,10 +289,10 @@ class ['a] list_selection_box (listref : 'a list ref)
 
     initializer
       (** create the functions called when the buttons are clicked *)
-      let f_add () = 
+      let f_add () =
         (* get the files to add with the function provided *)
         let l = add_function () in
-        (* remove from the list the ones which are already in 
+        (* remove from the list the ones which are already in
            the listref, using the eq predicate *)
         let l2 = List.fold_left
             (fun acc -> fun ele ->
@@ -293,7 +302,7 @@ class ['a] list_selection_box (listref : 'a list ref)
                 acc @ [ele])
             !listref
             l
-        in    
+        in
         self#update l2
       in
       let f_remove () =
@@ -309,14 +318,19 @@ class ['a] list_selection_box (listref : 'a list ref)
         let new_list = iter 0 !listref in
         self#update new_list
       in
+      let _ = dbg "list_selection_box: connecting wb_add" in
       (* connect the functions to the buttons *)
       ignore (wb_add#connect#clicked f_add);
+      let _ = dbg "list_selection_box: connecting wb_remove" in
       ignore (wb_remove#connect#clicked f_remove);
+      let _ = dbg "list_selection_box: connecting wb_up" in
       ignore (wb_up#connect#clicked (fun () -> self#up_selected));
       (
        match f_edit_opt with
 	 None -> ()
-       | Some f -> ignore (wb_edit#connect#clicked (fun () -> self#edit_selected f))
+       | Some f ->
+	   let _ = dbg "list_selection_box: connecting wb_edit" in
+	   ignore (wb_edit#connect#clicked (fun () -> self#edit_selected f))
       );
       (* connect the selection and deselection of items in the clist *)
       let f_select ~row ~column ~event =
@@ -335,7 +349,9 @@ class ['a] list_selection_box (listref : 'a list ref)
             ()
       in
       (* connect the select and deselect events *)
+      let _ = dbg "list_selection_box: connecting select_row" in
       ignore(wlist#connect#select_row f_select);
+      let _ = dbg "list_selection_box: connecting unselect_row" in
       ignore(wlist#connect#unselect_row f_unselect);
 
       (* initialize the clist with the listref *)
@@ -344,7 +360,8 @@ class ['a] list_selection_box (listref : 'a list ref)
 
 
 (** This class is used to build a box for a string parameter.*)
-class string_param_box param =
+class string_param_box param (tt:GData.tooltips) =
+  let _ = dbg "string_param_box" in
   let hbox = GPack.hbox () in
   let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
   let wl = GMisc.label ~text: param.string_label ~packing: wev#add () in
@@ -353,22 +370,20 @@ class string_param_box param =
       ~packing: (hbox#pack ~expand: param.string_expand ~padding: 2)
       ()
   in
-  let _ = 
+  let _ =
     match param.string_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 
+	tt#set_tip ~text: help ~privat: help wev#coerce
   in
-  let _ = we#set_text param.string_value in
+  let _ = we#set_text (param.string_to_string param.string_value) in
 
   object (self)
     (** This method returns the main box ready to be packed. *)
     method box = hbox#coerce
     (** This method applies the new value of the parameter. *)
     method apply =
-      let new_value = we#text in
+      let new_value = param.string_of_string we#text in
       if new_value <> param.string_value then
 	let _ = param.string_f_apply new_value in
 	param.string_value <- new_value
@@ -377,24 +392,23 @@ class string_param_box param =
   end ;;
 
 (** This class is used to build a box for a combo parameter.*)
-class combo_param_box param =
+class combo_param_box param (tt:GData.tooltips) =
+  let _ = dbg "combo_param_box" in
   let hbox = GPack.hbox () in
   let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
   let wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in
   let wc = GEdit.combo
       ~popdown_strings: param.combo_choices
       ~value_in_list: (not param.combo_new_allowed)
-(*      ~ok_if_empty: param.combo_blank_allowed*)
+      (* ~allow_empty: param.combo_blank_allowed *)
       ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
       ()
   in
-  let _ = 
+  let _ =
     match param.combo_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 
+	tt#set_tip ~text: help ~privat: help wev#coerce
   in
   let _ = wc#entry#set_editable param.combo_editable in
   let _ = wc#entry#set_text param.combo_value in
@@ -413,8 +427,9 @@ class combo_param_box param =
   end ;;
 
 (** Class used to pack a custom box. *)
-class custom_param_box param =
-  let top = 
+class custom_param_box param (tt:GData.tooltips) =
+  let _ = dbg "custom_param_box" in
+  let top =
     match param.custom_framed with
       None -> param.custom_box#coerce
     | Some l ->
@@ -428,40 +443,39 @@ class custom_param_box param =
   end
 
 (** This class is used to build a box for a color parameter.*)
-class color_param_box param =
+class color_param_box param (tt:GData.tooltips) =
+  let _ = dbg "color_param_box" in
   let v = ref param.color_value in
   let hbox = GPack.hbox () in
-  let wb = GButton.button ~label: param.color_label 
-      ~packing: (hbox#pack ~expand: false ~padding: 2) () 
+  let wb = GButton.button ~label: param.color_label
+      ~packing: (hbox#pack ~expand: false ~padding: 2) ()
   in
-  let w_test = GMisc.arrow 
+  let w_test = GMisc.arrow
       ~kind: `RIGHT
       ~shadow: `OUT
       ~width: 20
       ~height: 20
       ~packing: (hbox#pack ~expand: false ~padding: 2 )
-      () 
+      ()
   in
   let we = GEdit.entry
       ~editable: param.color_editable
       ~packing: (hbox#pack ~expand: param.color_expand ~padding: 2)
       ()
   in
-  let _ = 
+  let _ =
     match param.color_help with
       None -> ()
     | Some help ->
-	let tooltips = GData.tooltips () in
-	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
-	tooltips#set_tip wb#coerce ~text: help ~privat: help 
+	tt#set_tip ~text: help ~privat: help wb#coerce
   in
   let set_color s =
     let style = w_test#misc#style#copy in
     (
-     try style#set_bg [ (`NORMAL, `NAME s) ; ]
+     try style#set_fg [ (`NORMAL, `NAME s) ; ]
      with _ -> ()
     );
-    w_test#misc#set_style style 
+    w_test#misc#set_style style;
   in
   let _ = set_color !v in
   let _ = we#set_text !v in
@@ -476,26 +490,25 @@ class color_param_box param =
     let wb_cancel = dialog#cancel_button in
     let _ = dialog#connect#destroy GMain.Main.quit in
     let _ = wb_ok#connect#clicked
-	(fun () -> 
-	  (* let color = dialog#colorsel#get_color in
-	  let r = int_of_float (ceil (color.Gtk.red *. 255.)) in
-	  let g = int_of_float (ceil (color.Gtk.green *. 255.)) in
-	  let b = int_of_float (ceil (color.Gtk.blue *. 255.)) in
-	  let s = Printf.sprintf "#%2X%2X%2X" r g b in
-	  let _ = 
+	(fun () ->
+(*	  let color = dialog#colorsel#color in
+	  let r = (Gdk.Color.red color) in
+	  let g = (Gdk.Color.green color)in
+	  let b = (Gdk.Color.blue color) in
+	  let s = Printf.sprintf "#%4X%4X%4X" r g b in
+	  let _ =
 	    for i = 1 to (String.length s) - 1 do
 	      if s.[i] = ' ' then s.[i] <- '0'
 	    done
 	  in
-	  we#set_text s ;
-	  set_color s;*)
+	  we#set_text s ; *)
 	  dialog#destroy ()
 	)
     in
     let _ = wb_cancel#connect#clicked dialog#destroy in
     GMain.Main.main ()
   in
-  let _ = 
+  let _ =
     if param.color_editable then ignore (wb#connect#clicked f_sel)
   in
 
@@ -510,27 +523,30 @@ class color_param_box param =
 	param.color_value <- new_value
       else
 	()
+
+    initializer
+      ignore (we#connect#changed (fun () -> set_color we#text));
+
   end ;;
 
 (** This class is used to build a box for a font parameter.*)
-class font_param_box param =
+class font_param_box param (tt:GData.tooltips) =
+  let _ = dbg "font_param_box" in
   let v = ref param.font_value in
   let hbox = GPack.hbox () in
-  let wb = GButton.button ~label: param.font_label 
-      ~packing: (hbox#pack ~expand: false ~padding: 2) () 
+  let wb = GButton.button ~label: param.font_label
+      ~packing: (hbox#pack ~expand: false ~padding: 2) ()
   in
   let we = GEdit.entry
       ~editable: false
       ~packing: (hbox#pack ~expand: param.font_expand ~padding: 2)
       ()
   in
-  let _ = 
+  let _ =
     match param.font_help with
       None -> ()
     | Some help ->
-	let tooltips = GData.tooltips () in
-	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
-	tooltips#set_tip wb#coerce ~text: help ~privat: help 
+	tt#set_tip ~text: help ~privat: help wb#coerce
   in
   let set_entry_font font_opt =
     match font_opt with
@@ -538,7 +554,7 @@ class font_param_box param =
     | Some s ->
 	let style = we#misc#style#copy in
 	(
-	 try 
+	 try
 	   let font = Gdk.Font.load_fontset s in
 	   style#set_font font
 	 with _ -> ()
@@ -559,10 +575,10 @@ class font_param_box param =
     let wb_cancel = dialog#cancel_button in
     let _ = dialog#connect#destroy GMain.Main.quit in
     let _ = wb_ok#connect#clicked
-	(fun () -> 
-	  let font_opt = dialog#selection#font_name in
-(*	  we#set_text (match font_opt with None -> "" | Some s -> s) ;
-	  set_entry_font font_opt;*)
+	(fun () ->
+	  let font = dialog#selection#font_name in
+	  we#set_text font ;
+	  set_entry_font (Some font);
 	  dialog#destroy ()
 	)
     in
@@ -585,79 +601,89 @@ class font_param_box param =
   end ;;
 
 (** This class is used to build a box for a text parameter.*)
-class text_param_box param =
-  let hbox = GPack.hbox ~height: 100 () in
-  let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
-  let wl = GMisc.label ~text: param.string_label ~packing: wev#add () in
+class text_param_box param (tt:GData.tooltips) =
+  let _ = dbg "text_param_box" in
+  let wf = GBin.frame ~label: param.string_label ~height: 100 () in
+  let wev = GBin.event_box ~packing: wf#add () in
   let wscroll = GBin.scrolled_window
       ~vpolicy: `AUTOMATIC
       ~hpolicy: `AUTOMATIC
-      ~packing: (hbox#pack ~expand: true ~padding: 2) () 
+      ~packing: wev#add ()
   in
-  let wt = GText.view ~packing:wscroll#add () in
-(*   let _ = wt#coerce#misc#set_size_request ~height:100 in *)
-  let _ = wt#set_editable param.string_editable in
-  let _ = 
+  let wview = GText.view
+      ~editable: param.string_editable
+      ~packing: wscroll#add
+      ()
+  in
+  let _ =
     match param.string_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 
+	tt#set_tip ~text: help ~privat: help wev#coerce
   in
-  let _ = wt#buffer#insert param.string_value in
+  let _ = dbg "text_param_box: buffer creation" in
+  let buffer = GText.buffer () in
 
+  let _ = wview#set_buffer buffer in
+  let _ = buffer#insert (param.string_to_string param.string_value) in
+  let _ = dbg "text_param_box: object(self)" in
   object (self)
-    val wt = wt
+    val wview = wview
     (** This method returns the main box ready to be packed. *)
-    method box = hbox#coerce
+    method box = wf#coerce
     (** This method applies the new value of the parameter. *)
     method apply =
-      let new_value = wt#buffer#get_text () in
-      if new_value <> param.string_value then
-	let _ = param.string_f_apply new_value in
-	param.string_value <- new_value
+      let v = param.string_of_string (buffer#get_text ()) in
+      if v <> param.string_value then
+	(
+	 dbg "apply new value !";
+	 let _ = param.string_f_apply v in
+	 param.string_value <- v
+	)
       else
 	()
   end ;;
 
 (** This class is used to build a box a html parameter. *)
-class html_param_box param =
+class html_param_box param (tt:GData.tooltips) =
+  let _ = dbg "html_param_box" in
   object (self)
-    inherit text_param_box param
+    inherit text_param_box param tt
 
     method private exec html_start html_end () =
-      let s,e = wt#buffer#selection_bounds in
-      if s#compare e = 0 then 
-	wt#buffer#insert (html_start^html_end)
-      else begin
-	ignore (wt#buffer#insert ~iter:e html_end);
-	ignore (wt#buffer#insert ~iter:s html_start);
-	wt#buffer#place_cursor 
-	  (e#forward_chars (String.length (html_start^html_end)))
-      end
+      let (i1,i2) = wview#buffer#selection_bounds in
+      let s = i1#get_text ~stop: i2 in
+      match s with
+	"" ->
+	  wview#buffer#insert (html_start^html_end)
+      |	_ ->
+	  ignore (wview#buffer#insert ~iter: i2 html_end);
+	  ignore (wview#buffer#insert ~iter: i1 html_start);
+	  wview#buffer#place_cursor ~where: i2
+
     initializer
+      dbg "html_param_box:initializer";
       let (_,html_bindings) = html_config_file_and_option () in
+      dbg "html_param_box:connecting key press events";
       let add_shortcut hb =
 	let (mods, k) = hb.html_key in
-	Okey.add wt ~mods k (self#exec hb.html_begin hb.html_end)
+	Okey.add wview ~mods k (self#exec hb.html_begin hb.html_end)
       in
-      List.iter add_shortcut (O.(!!) html_bindings)      
+      List.iter add_shortcut html_bindings#get;
+      dbg "html_param_box:end"
   end
 
 (** This class is used to build a box for a boolean parameter.*)
-class bool_param_box param =
+class bool_param_box param (tt:GData.tooltips) =
+  let _ = dbg "bool_param_box" in
   let wchk = GButton.check_button
       ~label: param.bool_label
       ()
   in
-  let _ = 
+  let _ =
     match param.bool_help with
       None -> ()
-    | Some help ->
-	let tooltips = GData.tooltips () in
-	ignore (wchk#connect#destroy ~callback: tooltips#destroy);
-	tooltips#set_tip wchk#coerce ~text: help ~privat: help 
+    | Some help -> tt#set_tip ~text: help ~privat: help wchk#coerce
   in
   let _ = wchk#set_active param.bool_value in
   let _ = wchk#misc#set_sensitive param.bool_editable in
@@ -676,25 +702,24 @@ class bool_param_box param =
   end ;;
 
 (** This class is used to build a box for a file name parameter.*)
-class filename_param_box param =
+class filename_param_box param (tt:GData.tooltips) =
+  let _ = dbg "filename_param_box" in
   let hbox = GPack.hbox () in
-  let wb = GButton.button ~label: param.string_label 
-      ~packing: (hbox#pack ~expand: false ~padding: 2) () 
+  let wb = GButton.button ~label: param.string_label
+      ~packing: (hbox#pack ~expand: false ~padding: 2) ()
   in
   let we = GEdit.entry
       ~editable: param.string_editable
       ~packing: (hbox#pack ~expand: param.string_expand ~padding: 2)
       ()
   in
-  let _ = 
+  let _ =
     match param.string_help with
       None -> ()
     | Some help ->
-	let tooltips = GData.tooltips () in
-	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
-	tooltips#set_tip wb#coerce ~text: help ~privat: help 
+	tt#set_tip ~text: help ~privat: help wb#coerce
   in
-  let _ = we#set_text param.string_value in
+  let _ = we#set_text (param.string_to_string param.string_value) in
 
   let f_click () =
     match select_files param.string_label with
@@ -703,7 +728,7 @@ class filename_param_box param =
     | f :: _ ->
         we#set_text f
   in
-  let _ = 
+  let _ =
     if param.string_editable then
       let _ = wb#connect#clicked f_click in
       ()
@@ -716,7 +741,7 @@ class filename_param_box param =
     method box = hbox#coerce
     (** This method applies the new value of the parameter. *)
     method apply =
-      let new_value = we#text in
+      let new_value = param.string_of_string we#text in
       if new_value <> param.string_value then
 	let _ = param.string_f_apply new_value in
 	param.string_value <- new_value
@@ -725,11 +750,12 @@ class filename_param_box param =
   end ;;
 
 (** This class is used to build a box for a hot key parameter.*)
-class hotkey_param_box param =
+class hotkey_param_box param (tt:GData.tooltips) =
+  let _ = dbg "hotkey_param_box" in
   let hbox = GPack.hbox () in
   let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
-  let wl = GMisc.label ~text: param.hk_label 
-      ~packing: wev#add () 
+  let wl = GMisc.label ~text: param.hk_label
+      ~packing: wev#add ()
   in
   let we = GEdit.entry
       ~editable: false
@@ -737,15 +763,13 @@ class hotkey_param_box param =
       ()
   in
   let value = ref param.hk_value in
-  let _ = 
+  let _ =
     match param.hk_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 
+	tt#set_tip ~text: help ~privat: help wev#coerce
   in
-  let _ = we#set_text (KeyOption.key_to_string param.hk_value) in
+  let _ = we#set_text (Configwin_types.key_to_string param.hk_value) in
   let mods_we_dont_care = [`MOD2 ; `MOD3 ; `MOD4 ; `MOD5 ; `LOCK] in
   let capture ev =
     let key = GdkEvent.Key.keyval ev in
@@ -755,10 +779,10 @@ class hotkey_param_box param =
 	modifiers
     in
     value := (mods, key);
-    we#set_text (KeyOption.key_to_string !value);
+    we#set_text (Glib.Convert.locale_to_utf8 (Configwin_types.key_to_string !value));
     false
   in
-  let _ = 
+  let _ =
     if param.hk_editable then
       ignore (we#event#connect#key_press capture)
     else
@@ -798,7 +822,7 @@ class modifiers_param_box param =
 	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
 	tooltips#set_tip wev#coerce ~text: help ~privat: help 
   in
-  let _ = we#set_text (KeyOption.modifiers_to_string param.md_value) 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
@@ -807,7 +831,7 @@ class modifiers_param_box param =
 	modifiers
     in
     value := mods;
-    we#set_text (KeyOption.modifiers_to_string !value);
+    we#set_text (Configwin_types.modifiers_to_string !value);
     false
   in
   let _ = 
@@ -831,35 +855,35 @@ class modifiers_param_box param =
   end ;;
 
 (** This class is used to build a box for a date parameter.*)
-class date_param_box param =
+class date_param_box param (tt:GData.tooltips) =
+  let _ = dbg "date_param_box" in
   let v = ref param.date_value in
   let hbox = GPack.hbox () in
-  let wb = GButton.button ~label: param.date_label 
-      ~packing: (hbox#pack ~expand: false ~padding: 2) () 
+  let wb = GButton.button ~label: param.date_label
+      ~packing: (hbox#pack ~expand: false ~padding: 2) ()
   in
   let we = GEdit.entry
       ~editable: false
       ~packing: (hbox#pack ~expand: param.date_expand ~padding: 2)
       ()
   in
-  let _ = 
+
+  let _ =
     match param.date_help with
       None -> ()
     | Some help ->
-	let tooltips = GData.tooltips () in
-	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
-	tooltips#set_tip wb#coerce ~text: help ~privat: help 
+	tt#set_tip ~text: help ~privat: help wb#coerce
   in
-  let _ = we#set_text (param.date_f_string param.date_value) in
 
+  let _ = we#set_text (param.date_f_string param.date_value) in
   let f_click () =
     match select_date param.date_label !v with
       None -> ()
-    | Some (y,m,d) -> 
+    | Some (y,m,d) ->
 	v := (d,m,y) ;
 	we#set_text (param.date_f_string (d,m,y))
   in
-  let _ = 
+  let _ =
     if param.date_editable then
       let _ = wb#connect#clicked f_click in
       ()
@@ -880,7 +904,8 @@ class date_param_box param =
   end ;;
 
 (** This class is used to build a box for a parameter whose values are a list.*)
-class ['a] list_param_box (param : 'a list_param) =
+class ['a] list_param_box (param : 'a list_param) (tt:GData.tooltips) =
+  let _ = dbg "list_param_box" in
   let listref = ref param.list_value in
   let frame_selection = new list_selection_box
       listref
@@ -891,8 +916,9 @@ class ['a] list_param_box (param : 'a list_param) =
       param.list_color
       param.list_eq
       param.list_f_add param.list_label param.list_editable
+      tt
   in
-      
+
   object (self)
     (** This method returns the main box ready to be packed. *)
     method box = frame_selection#box#coerce
@@ -902,75 +928,75 @@ class ['a] list_param_box (param : 'a list_param) =
       param.list_value <- !listref
   end ;;
 
-(** This class is used to build a box from a configuration structure 
+(** This class is used to build a box from a configuration structure
    and adds the page to the given notebook. *)
-class configuration_box conf_struct (notebook : GPack.notebook) =
+class configuration_box (tt:GData.tooltips) conf_struct (notebook : GPack.notebook) =
   (* we build different widgets, according to the conf_struct parameter *)
   let main_box = GPack.vbox () in
-  let (label, child_boxes) = 
+  let (label, child_boxes) =
     match conf_struct with
       Section (label, param_list) ->
 	let f parameter =
-	      match parameter with
-		String_param p ->
-		  let box = new string_param_box p in
-		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
-		  box
-	      |	Combo_param p ->
-		  let box = new combo_param_box p in
-		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
-		  box
-	      |	Text_param p ->
-		  let box = new text_param_box p in
-		  let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
-		  box
-	      | Bool_param p ->
-		  let box = new bool_param_box p in
-		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
-		  box
-	      |	Filename_param p ->
-		  let box = new filename_param_box p in
-		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
-		  box
-	      |	List_param f ->
-		  let box = f () in
-		  let _ = main_box#pack ~expand: true ~padding: 2 box#box in
-		  box
-	      |	Custom_param p ->
-		  let box = new custom_param_box p in
-		  let _ = main_box#pack ~expand: p.custom_expand ~padding: 2 box#box in
-		  box
-	      |	Color_param p ->
-		  let box = new color_param_box p in
-		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
-		  box
-	      |	Font_param p ->
-		  let box = new font_param_box p in
-		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
-		  box
-	      |	Date_param p ->
-		  let box = new date_param_box p in
-		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
-		  box
-	      |	Hotkey_param p ->
-		  let box = new hotkey_param_box p in
-		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
-		  box
-	      |	Modifiers_param p ->
-		  let box = new modifiers_param_box p in
-		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
-		  box
-	      |	Html_param p ->
-		  let box = new html_param_box p in
-		  let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
-		  box
+	  match parameter with
+	    String_param p ->
+	      let box = new string_param_box p tt in
+	      let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	      box
+	  | Combo_param p ->
+	      let box = new combo_param_box p tt in
+	      let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	      box
+	  | Text_param p ->
+	      let box = new text_param_box p tt in
+	      let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
+	      box
+	  | Bool_param p ->
+	      let box = new bool_param_box p tt in
+	      let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	      box
+	  | Filename_param p ->
+	      let box = new filename_param_box p tt in
+	      let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	      box
+	  | List_param f ->
+	      let box = f tt in
+	      let _ = main_box#pack ~expand: true ~padding: 2 box#box in
+	      box
+	  | Custom_param p ->
+	      let box = new custom_param_box p tt in
+	      let _ = main_box#pack ~expand: p.custom_expand ~padding: 2 box#box in
+	      box
+	  | Color_param p ->
+	      let box = new color_param_box p tt in
+	      let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	      box
+	  | Font_param p ->
+	      let box = new font_param_box p tt in
+	      let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	      box
+	  | Date_param p ->
+	      let box = new date_param_box p tt in
+	      let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	      box
+	  | Hotkey_param p ->
+	      let box = new hotkey_param_box p tt in
+	      let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	      box
+	  | Modifiers_param p ->
+	      let box = new modifiers_param_box p in
+	      let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+		box
+	  | Html_param p ->
+	      let box = new html_param_box p tt in
+	      let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
+	      box
 	in
 	let list_children_boxes = List.map f param_list in
-	
+
 	(label, list_children_boxes)
 
     | Section_list (label, struct_list) ->
-	let wnote = GPack.notebook 
+	let wnote = GPack.notebook
             (*homogeneous_tabs: true*)
 	    ~scrollable: true
 	    ~show_tabs: true
@@ -980,15 +1006,15 @@ class configuration_box conf_struct (notebook : GPack.notebook) =
 	in
 	(* we create all the children boxes *)
 	let f structure =
-	  let new_box = new configuration_box structure wnote in
+	  let new_box = new configuration_box tt structure wnote in
 	  new_box
 	in
 	let list_child_boxes = List.map f struct_list in
 	(label, list_child_boxes)
-	
+
   in
   let page_label = GMisc.label ~text: label () in
-  let _ = notebook#append_page 
+  let _ = notebook#append_page
       ~tab_label: page_label#coerce
       main_box#coerce
   in
@@ -1008,9 +1034,9 @@ class configuration_box conf_struct (notebook : GPack.notebook) =
    Before calling the callback of a button, the [apply] function
    of each parameter is called.
 *)
-let tabbed_box conf_struct_list buttons =
+let tabbed_box conf_struct_list buttons tooltips =
   let vbox = GPack.vbox () in
-  let wnote = GPack.notebook 
+  let wnote = GPack.notebook
       (*homogeneous_tabs: true*)
       ~scrollable: true
       ~show_tabs: true
@@ -1018,18 +1044,19 @@ let tabbed_box conf_struct_list buttons =
       ~packing: (vbox#pack ~expand: true)
       ()
   in
-  let list_param_box = 
-    List.map (fun conf_struct -> new configuration_box conf_struct wnote)
+  let list_param_box =
+    List.map
+      (fun conf_struct -> new configuration_box tooltips conf_struct wnote)
       conf_struct_list
   in
-  let f_apply () = 
+  let f_apply () =
     List.iter (fun param_box -> param_box#apply) list_param_box  ;
   in
   let hbox_buttons = GPack.hbox ~packing: (vbox#pack ~expand: false ~padding: 4) () in
   let rec iter_buttons ?(grab=false) = function
       [] ->
         ()
-    | (label, callb) :: q ->    
+    | (label, callb) :: q ->
         let b = GButton.button ~label: label
             ~packing:(hbox_buttons#pack ~expand:true ~fill: true ~padding:4) ()
         in
@@ -1046,127 +1073,110 @@ let tabbed_box conf_struct_list buttons =
 
 (** This function takes a configuration structure list and creates a window
    to configure the various parameters. *)
-let edit ?(with_apply=true)  
+let edit ?(with_apply=true)
     ?(apply=(fun () -> ()))
-    title ?(width=400) ?(height=400) 
+    title ?(width=400) ?(height=400)
     conf_struct_list =
-  let return = ref Return_cancel in
-  let window = GWindow.window
-		 ~position:`CENTER
-      ~modal: true ~title: title
-      ~width: width ~height: height ()
-  in
-  let _ = window#connect#destroy ~callback: GMain.Main.quit in
-  let vbox = GPack.vbox ~packing: window#add () in
-  let wnote = GPack.notebook 
-      (*homogeneous_tabs: true*)
-      ~scrollable: true
-      ~show_tabs: true
-      ~tab_border: 3
-      ~packing: (vbox#pack ~expand: true)
-      ()
-  in
-  let list_param_box = 
-    List.map (fun conf_struct -> new configuration_box conf_struct wnote)
+  let dialog = GWindow.dialog
+    ~position:`CENTER
+    ~modal: true ~title: title
+    ~height ~width
+    ()
+  in
+  let tooltips = GData.tooltips () in
+  let wnote = GPack.notebook
+    (*homogeneous_tabs: true*)
+    ~scrollable: true
+    ~show_tabs: true
+    ~tab_border: 3
+    ~packing: (dialog#vbox#pack ~expand: true)
+    ()
+  in
+  let list_param_box =
+    List.map
+      (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 ()
+    in
+    let f_ok () =
+      List.iter (fun param_box -> param_box#apply) list_param_box  ;
+      Return_ok
+    in
+    let destroy () =
+      tooltips#destroy () ;
+      dialog#destroy ();
+    in
+    let rec iter rep =
+      try
+	match dialog#run () with
+	  | `APPLY  -> f_apply (); iter Return_apply
+	  | `OK -> destroy (); f_ok ()
+	  | _ -> destroy (); rep
+      with
+	  Failure s ->
+	    GToolbox.message_box "Error" s; iter rep
+	| e ->
+	    GToolbox.message_box "Error" (Printexc.to_string e); iter rep
+    in
+      iter Return_cancel
 
-  let hbox_buttons = GPack.hbox ~packing: (vbox#pack ~expand: false ~padding: 4) () in
-  let bApply = GButton.button
-		 ~stock:`APPLY
-		 ~label: Configwin_messages.mApply
-		 ()
-  in
-  if with_apply then hbox_buttons#pack ~expand: true ~padding: 3 bApply#coerce;
-  let bOk = GButton.button
-	      ~stock:`OK
-      ~label: Configwin_messages.mOk
-      ~packing: (hbox_buttons#pack ~expand: true ~padding: 3)
-      ()
-  in
-  let bCancel = GButton.button
-		  ~stock:`CANCEL
-      ~label: Configwin_messages.mCancel
-      ~packing: (hbox_buttons#pack ~expand: true ~padding: 3)
-      ()
-  in
-  (* we connect the click on the apply button *)
-  let f_apply () = 
-    List.iter (fun param_box -> param_box#apply) list_param_box  ;
-    apply ();
-    return := Return_apply
-  in
-  let _ = bApply#connect#clicked f_apply in
-  (* we connect the click on the ok button : the same than apply but we then close the window *)
-  let f_ok () = 
-    List.iter (fun param_box -> param_box#apply) list_param_box  ;
-    return := Return_ok ;
-    window#destroy () 
-  in
-  let _ = bOk#connect#clicked f_ok in
-  (* we connect the click on the cancel button : close the window *)
-  let f_cancel () = window#destroy () in
-  let _ = bCancel#connect#clicked f_cancel in
-
-  let _ = window#event#connect#key_press ~callback:
-	    (fun k -> if GdkEvent.Key.keyval k = GdkKeysyms._Escape then f_cancel ();false)
-  in
-  let _ = window#show () in
-  GMain.Main.main () ;
-  !return
-
-
-(** Create a vbox with the list of given parameters,
-   and the given list of buttons (defined by their label and callback).
-   Before calling the callback of a button, the [apply] function
-   of each parameter is called.
-*)
-let box param_list buttons =
+(** Create a vbox with the list of given parameters. *)
+let box param_list tt =
   let main_box = GPack.vbox  () in
   let f parameter =
     match parameter with
       String_param p ->
-	let box = new string_param_box p in
+	let box = new string_param_box p tt in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
     | Combo_param p ->
-	let box = new combo_param_box p in
+	let box = new combo_param_box p tt in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
     | Text_param p ->
-	let box = new text_param_box p in
+	let box = new text_param_box p tt in
 	let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
 	box
     | Bool_param p ->
-	let box = new bool_param_box p in
+	let box = new bool_param_box p tt in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
     | Filename_param p ->
-	let box = new filename_param_box p in
+	let box = new filename_param_box p tt in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
     | List_param f ->
-	let box = f () in
+	let box = f tt in
 	let _ = main_box#pack ~expand: true ~padding: 2 box#box in
 	box
     | Custom_param p ->
-	let box = new custom_param_box p in
+	let box = new custom_param_box p tt in
 	let _ = main_box#pack ~expand: p.custom_expand ~padding: 2 box#box in
 	box
     | Color_param p ->
-	let box = new color_param_box p in
+	let box = new color_param_box p tt in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
     | Font_param p ->
-	let box = new font_param_box p in
+	let box = new font_param_box p tt in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
     | Date_param p ->
-	let box = new date_param_box p in
+	let box = new date_param_box p tt in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
     | Hotkey_param p ->
-	let box = new hotkey_param_box p in
+	let box = new hotkey_param_box p tt in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
     | Modifiers_param p ->
@@ -1174,70 +1184,61 @@ let box param_list buttons =
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
     | Html_param p ->
-	let box = new html_param_box p in
+	let box = new html_param_box p tt in
 	let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
 	box
   in
   let list_param_box = List.map f param_list in
-  let f_apply () = 
-    List.iter (fun param_box -> param_box#apply) list_param_box 
+  let f_apply () =
+    List.iter (fun param_box -> param_box#apply) list_param_box
   in
-  let hbox_buttons = GPack.hbox ~packing: (main_box#pack ~expand: false ~padding: 4) () in
-  let rec iter_buttons ?(grab=false) = function
-      [] ->
-        ()
-    | (label, callb) :: q ->    
-        let b = GButton.button ~label: label
-            ~packing:(hbox_buttons#pack ~expand:true ~fill: true ~padding:4) ()
-        in
-        ignore (b#connect#clicked ~callback:
-		  (fun () -> f_apply (); callb ()));
-        (* If it's the first button then give it the focus *)
-        if grab then b#grab_default ();
+  (main_box, f_apply)
 
-        iter_buttons q
+(** This function takes a list of parameter specifications and
+   creates a window to configure the various parameters.*)
+let simple_edit ?(with_apply=true)
+    ?(apply=(fun () -> ()))
+    title ?width ?height
+    param_list =
+  let dialog = GWindow.dialog
+      ~modal: true ~title: title
+      ?height ?width
+      ()
   in
-  iter_buttons ~grab: true buttons;
+  let tooltips = GData.tooltips () in
+  if with_apply then
+    dialog#add_button Configwin_messages.mApply `APPLY;
 
-  main_box
+  dialog#add_button Configwin_messages.mOk `OK;
+  dialog#add_button Configwin_messages.mCancel `CANCEL;
 
+  let (box, f_apply) = box param_list tooltips in
+  dialog#vbox#pack ~expand: true ~fill: true box#coerce;
 
-(** This function takes a list of parameter specifications and 
-   creates a window to configure the various parameters.*)
-let simple_edit ?(with_apply=true)  
-    ?(apply=(fun () -> ()))
-    title ?width ?height 
-    param_list =
-  let return = ref Return_cancel in
-  let window = GWindow.window ~modal: true ~title: title () in
-  let _ = match width, height with
-    None, None -> ()
-  | Some w, None -> window#misc#set_size_request ~width: w ()
-  | None, Some h -> window#misc#set_size_request ~height: h ()
-  | Some w, Some h -> window#misc#set_size_request ~width: w ~height: h ()
-  in
-  let _ = window#connect#destroy ~callback: GMain.Main.quit in
-  let buttons = 
-    (if with_apply then
-      [Configwin_messages.mApply, fun () -> apply (); return := Return_apply]
-    else
-      []
-    ) @ [
-	(Configwin_messages.mOk, fun () -> return := Return_ok ; window#destroy ()) ;
-	(Configwin_messages.mCancel, window#destroy) ;
-      ]	
+  let destroy () =
+    tooltips#destroy () ;
+    dialog#destroy ();
   in
-  let box = box param_list buttons in
-  window#add box#coerce;
-  let _ = window#show () in
-  GMain.Main.main () ;
-  !return
+  let rec iter rep =
+    try
+      match dialog#run () with
+      | `APPLY  -> f_apply (); apply (); iter Return_apply
+      | `OK -> f_apply () ; destroy () ; Return_ok
+      | _ -> destroy (); rep
+    with
+      Failure s ->
+	GToolbox.message_box "Error" s; iter rep
+    | e ->
+	GToolbox.message_box "Error" (Printexc.to_string e); iter rep
+  in
+  iter Return_cancel
+
 
 let edit_string l s =
   match GToolbox.input_string ~title: l ~text: s Configwin_messages.mValue with
     None -> s
   | Some s2 -> s2
-  
+
 (** Create a string param. *)
 let string ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
   String_param
@@ -1248,7 +1249,25 @@ let string ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       string_editable = editable ;
       string_f_apply = f ;
       string_expand = expand ;
-    } 
+      string_to_string = (fun x -> x) ;
+      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 =
@@ -1263,14 +1282,14 @@ let bool ?(editable=true) ?help ?(f=(fun _ -> ())) label v =
 
 (** Create a list param. *)
 let list ?(editable=true) ?help
-    ?(f=(fun (_:'a list) -> ())) 
+    ?(f=(fun (_:'a list) -> ()))
     ?(eq=Pervasives.(=))
     ?(edit:('a -> 'a) option)
     ?(add=(fun () -> ([] : 'a list)))
     ?titles ?(color=(fun (_:'a) -> (None : string option)))
     label (f_strings : 'a -> string list) v =
   List_param
-    (fun () ->
+    (fun tt ->
       Obj.magic
 	(new list_param_box
 	   {
@@ -1285,13 +1304,14 @@ let list ?(editable=true) ?help
 	     list_f_edit = edit ;
 	     list_f_add = add ;
 	     list_f_apply = f ;
-	   } 
+	   }
+	   tt
 	)
     )
 
 (** Create a strings param. *)
 let strings ?(editable=true) ?help
-    ?(f=(fun _ -> ())) 
+    ?(f=(fun _ -> ()))
     ?(eq=Pervasives.(=))
     ?(add=(fun () -> [])) label v =
   list ~editable ?help ~f ~eq ~edit: (edit_string label) ~add label (fun s -> [s]) v
@@ -1321,8 +1341,8 @@ let font ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
     }
 
 (** Create a combo param. *)
-let combo ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) 
-    ?(new_allowed=false) 
+let combo ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ()))
+    ?(new_allowed=false)
     ?(blank_allowed=false) label choices v =
   Combo_param
     {
@@ -1338,7 +1358,7 @@ let combo ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ()))
     }
 
 (** Create a text param. *)
-let text ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v = 
+let text ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
   Text_param
     {
       string_label = label ;
@@ -1347,10 +1367,28 @@ let text ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       string_editable = editable ;
       string_f_apply = f ;
       string_expand = expand ;
-    } 
+      string_to_string = (fun x -> x) ;
+      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 = 
+let html ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
   Html_param
     {
       string_label = label ;
@@ -1359,10 +1397,12 @@ let html ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       string_editable = editable ;
       string_f_apply = f ;
       string_expand = expand ;
-    } 
+      string_to_string = (fun x -> x) ;
+      string_of_string = (fun x -> x) ;
+    }
 
 (** Create a filename param. *)
-let filename ?(editable=true) ?(expand=true)?help ?(f=(fun _ -> ())) label v = 
+let filename ?(editable=true) ?(expand=true)?help ?(f=(fun _ -> ())) label v =
   Filename_param
     {
       string_label = label ;
@@ -1371,17 +1411,19 @@ let filename ?(editable=true) ?(expand=true)?help ?(f=(fun _ -> ())) label v =
       string_editable = editable ;
       string_f_apply = f ;
       string_expand = expand ;
-    } 
+      string_to_string = (fun x -> x) ;
+      string_of_string = (fun x -> x) ;
+    }
 
 (** Create a filenames param.*)
-let filenames ?(editable=true) ?help ?(f=(fun _ -> ())) 
+let filenames ?(editable=true) ?help ?(f=(fun _ -> ()))
     ?(eq=Pervasives.(=))
     label v =
   let add () = select_files label in
-  list ~editable ?help ~f ~eq ~add label (fun s -> [s]) v
+  list ~editable ?help ~f ~eq ~add label (fun s -> [Glib.Convert.locale_to_utf8 s]) v
 
 (** Create a date param. *)
-let date ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) 
+let date ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ()))
     ?(f_string=(fun(d,m,y)-> Printf.sprintf "%d/%d/%d" y (m+1) d))
     label v =
   Date_param
@@ -1393,7 +1435,7 @@ let date ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ()))
       date_f_string = f_string ;
       date_f_apply = f ;
       date_expand = expand ;
-    } 
+    }
 
 (** Create a hot key param. *)
 let hotkey ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
@@ -1405,7 +1447,7 @@ let hotkey ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       hk_editable = editable ;
       hk_f_apply = f ;
       hk_expand = expand ;
-    } 
+    }
 
 let modifiers 
   ?(editable=true) 
@@ -1432,4 +1474,4 @@ let custom ?label box f expand =
       custom_f_apply = f ;
       custom_expand = expand ;
       custom_framed = label ;
-    } 
+    }
diff --git a/ide/utils/configwin_keys.ml b/ide/utils/configwin_keys.ml
index 9c867845..e1d7f33b 100644
--- a/ide/utils/configwin_keys.ml
+++ b/ide/utils/configwin_keys.ml
@@ -1,26 +1,27 @@
-(**************************************************************************)
-(*                   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                                *)
-(**************************************************************************)
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
 
 (** Key codes
 
diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml
index a6085138..f8984462 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/utils/configwin_messages.ml
@@ -1,31 +1,32 @@
-(**************************************************************************)
-(*                   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                                *)
-(**************************************************************************)
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
 
 (** Module containing the messages of Configwin.*)
 
 let software = "Configwin";;
-let version = "1.3";;
+let version = "1.2";;
 
 let html_config = "Configwin bindings configurator for html parameters"
 
diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml
index ee8ec70c..0def0b25 100644
--- a/ide/utils/configwin_types.ml
+++ b/ide/utils/configwin_types.ml
@@ -1,140 +1,148 @@
-(**************************************************************************)
-(*                   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                                *)
-(**************************************************************************)
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
 
 (** This module contains the types used in Configwin. *)
 
-open Uoptions
+open Config_file
 
-(** A module to define key options, with the {!Uoptions} module. *)
-module KeyOption = struct
-  let name_to_keysym = 
-    ("Button1", Configwin_keys.xk_Pointer_Button1) ::
-    ("Button2", Configwin_keys.xk_Pointer_Button2) ::
-    ("Button3", Configwin_keys.xk_Pointer_Button3) ::
-    ("Button4", Configwin_keys.xk_Pointer_Button4) ::
-    ("Button5", Configwin_keys.xk_Pointer_Button5) ::
-    Configwin_keys.name_to_keysym
-      
-  let string_to_key s =
-    let mask = ref [] in
-    let key = try
-      let pos = String.rindex s '-' in
-      for i = 0 to pos - 1 do 
-        let m = match s.[i] with
-          'C' -> `CONTROL
-        | 'S' -> `SHIFT
-        | 'L' -> `LOCK 
-        | 'M' -> `MOD1
-        | 'A' -> `MOD1
-        | '1' -> `MOD1
-        | '2' -> `MOD2
-        | '3' -> `MOD3
-        | '4' -> `MOD4
-        | '5' -> `MOD5
-        | _ -> 
-	    prerr_endline s;
-	    raise Not_found
-        in
-        mask := m :: !mask
-      done;
-      String.sub s (pos+1) (String.length s - pos - 1)
-    with _ -> 
-      s
-    in
-    try
-      !mask, List.assoc key name_to_keysym
-    with
-      e -> 
-	prerr_endline s;
-	raise e
-      
-  let key_to_string (m, k) =
-    let s = List.assoc k Configwin_keys.keysym_to_name in
-    match m with
-      [] -> s
-    | _ ->
-        let rec iter m s =
-          match m with
-            [] -> s
-          | c :: m ->
-              iter m ((
-                      match c with
-			`CONTROL -> "C"
-                      | `SHIFT -> "S"
-                      | `LOCK -> "L"
-                      | `MOD1 -> "A"
-                      | `MOD2 -> "2"
-                      | `MOD3 -> "3"
-                      | `MOD4 -> "4"
-                      | `MOD5 -> "5"
-                      | _  -> raise Not_found
-                     ) ^ s)
-        in
-        iter m ("-" ^ s)
+let name_to_keysym =
+  ("Button1", Configwin_keys.xk_Pointer_Button1) ::
+  ("Button2", Configwin_keys.xk_Pointer_Button2) ::
+  ("Button3", Configwin_keys.xk_Pointer_Button3) ::
+  ("Button4", Configwin_keys.xk_Pointer_Button4) ::
+  ("Button5", Configwin_keys.xk_Pointer_Button5) ::
+  Configwin_keys.name_to_keysym
+
+let string_to_key s =
+  let mask = ref [] in
+  let key = try
+    let pos = String.rindex s '-' in
+    for i = 0 to pos - 1 do
+      let m = match s.[i] with
+        'C' -> `CONTROL
+      | 'S' -> `SHIFT
+      | 'L' -> `LOCK
+      | 'M' -> `MOD1
+      | 'A' -> `MOD1
+      | '1' -> `MOD1
+      | '2' -> `MOD2
+      | '3' -> `MOD3
+      | '4' -> `MOD4
+      | '5' -> `MOD5
+      | _ ->
+	  prerr_endline s;
+	  raise Not_found
+      in
+      mask := m :: !mask
+    done;
+    String.sub s (pos+1) (String.length s - pos - 1)
+  with _ ->
+    s
+  in
+  try
+    !mask, List.assoc key name_to_keysym
+  with
+    e ->
+      prerr_endline s;
+      raise e
 
-  let modifiers_to_string m =
-    let rec iter m s =
-      match m with
+let key_to_string (m, k) =
+  let s = List.assoc k Configwin_keys.keysym_to_name in
+  match m with
+    [] -> s
+  | _ ->
+      let rec iter m s =
+        match m with
           [] -> s
         | c :: m ->
             iter m ((
-                      match c with
-			  `CONTROL -> "<ctrl>"
-			| `SHIFT -> "<shft>"
-			| `LOCK -> "<lock>"
-			| `MOD1 -> "<alt>"
-			| `MOD2 -> "<mod2>"
-			| `MOD3 -> "<mod3>"
-			| `MOD4 -> "<mod4>"
-			| `MOD5 -> "<mod5>"
-			| _  -> raise Not_found
-                    ) ^ s)
-    in
+                    match c with
+		      `CONTROL -> "C"
+                    | `SHIFT -> "S"
+                    | `LOCK -> "L"
+                    | `MOD1 -> "A"
+                    | `MOD2 -> "2"
+                    | `MOD3 -> "3"
+                    | `MOD4 -> "4"
+                    | `MOD5 -> "5"
+                    | _  -> raise Not_found
+                   ) ^ s)
+      in
+      iter m ("-" ^ s)
+
+let modifiers_to_string m =
+  let rec iter m s =
+    match m with
+        [] -> s
+      | c :: m ->
+          iter m ((
+                    match c with
+			`CONTROL -> "<ctrl>"
+		      | `SHIFT -> "<shft>"
+		      | `LOCK -> "<lock>"
+		      | `MOD1 -> "<alt>"
+		      | `MOD2 -> "<mod2>"
+		      | `MOD3 -> "<mod3>"
+		      | `MOD4 -> "<mod4>"
+		      | `MOD5 -> "<mod5>"
+		      | _  -> raise Not_found
+                  ) ^ s)
+  in
     iter m ""
-	  
-  let value_to_key v =
-    match v with
-      StringValue s -> string_to_key s
-    | _ -> 
-	prerr_endline "value_to_key";
-	raise Not_found
-	  
-  let key_to_value k =
-    StringValue (key_to_string k)
       
-  let (t : (Gdk.Tags.modifier list * int) option_class) = 
-    define_option_class "Key" value_to_key key_to_value
-end
+let value_to_key v =
+  match v with
+    Raw.String s -> string_to_key s
+  | _ ->
+      prerr_endline "value_to_key";
+      raise Not_found
+
+let key_to_value k =
+  Raw.String (key_to_string k)
+
+let key_cp_wrapper =
+  {
+    to_raw = key_to_value ;
+    of_raw = value_to_key ;
+  }
 
-(** This type represents a string or filename parameter. *)
-type string_param = {
+(** A class to define key options, with the {!Config_file} module. *)
+class key_cp =
+  [(Gdk.Tags.modifier list * int)] Config_file.cp_custom_type key_cp_wrapper
+
+(** This type represents a string or filename parameter, or
+   any other type, depending on the given conversion functions. *)
+type 'a string_param = {
     string_label : string; (** the label of the parameter *)
-    mutable string_value : string; (** the current value of the parameter *)
+    mutable string_value : 'a; (** the current value of the parameter *)
     string_editable : bool ; (** indicates if the value can be changed *)
-    string_f_apply : (string -> unit) ; (** the function to call to apply the new value of the parameter *)
+    string_f_apply : ('a -> unit) ; (** the function to call to apply the new value of the parameter *)
     string_help : string option ; (** optional help string *)
     string_expand : bool ; (** expand or not *)
+    string_to_string : 'a -> string ;
+    string_of_string : string -> 'a ;
   } ;;
 
 (** This type represents a boolean parameter. *)
@@ -214,14 +222,14 @@ type font_param = {
 
 type hotkey_param = {
     hk_label : string ; (** the label of the parameter *)
-    mutable hk_value : (Gdk.Tags.modifier list * int) ; 
+    mutable hk_value : (Gdk.Tags.modifier list * int) ;
              (** The value, as a list of modifiers and a key code *)
     hk_editable : bool ; (** indicates if the value can be changed *)
     hk_f_apply : ((Gdk.Tags.modifier list * int) -> unit) ;
              (** the function to call to apply the new value of the paramter *)
     hk_help : string option ; (** optional help string *)
     hk_expand : bool ; (** expand or not *)
-  } 
+  }
 
 type modifiers_param = {
     md_label : string ; (** the label of the parameter *)
@@ -235,13 +243,18 @@ type modifiers_param = {
     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. *)
 type parameter_kind =
-    String_param of string_param
-  | List_param of (unit -> <box: GObj.widget ; apply : unit>)
-  | Filename_param of string_param
+    String_param of string string_param
+  | List_param of (GData.tooltips -> <box: GObj.widget ; apply : unit>)
+  | Filename_param of string string_param
   | Bool_param of bool_param
-  | Text_param of string_param
+  | Text_param of string string_param
   | Combo_param of combo_param
   | Custom_param of custom_param
   | Color_param of color_param
@@ -249,7 +262,7 @@ type parameter_kind =
   | Font_param of font_param
   | Hotkey_param of hotkey_param
   | Modifiers_param of modifiers_param
-  | Html_param of string_param
+  | Html_param of string string_param
 ;;
 
 (** This type represents the structure of the configuration window. *)
@@ -273,27 +286,21 @@ type html_binding = {
     mutable html_key :  (Gdk.Tags.modifier list * int) ;
     mutable html_begin : string ;
     mutable html_end : string ;
-  } 
-
-module Html_binding = struct
-  let value_to_hb v =
-    match v with
-      List [StringValue hk ; StringValue debut; StringValue fin ]
-    | SmallList [StringValue hk ; StringValue debut; StringValue fin ] ->
-        { html_key = KeyOption.string_to_key hk ;
-	  html_begin = debut ;
-	  html_end = fin ;
-        }
-    | _ ->
-        prerr_endline "Html_binding.value_to_hb";
-        raise Not_found
+  }
 
-  let hb_to_value hb =
-    SmallList [ StringValue (KeyOption.key_to_string hb.html_key) ;
-                StringValue hb.html_begin ;
-                StringValue hb.html_end ;
-	      ]	
+let htmlbinding_cp_wrapper =
+  let w = Config_file.tuple3_wrappers
+      key_cp_wrapper
+      Config_file.string_wrappers
+      Config_file.string_wrappers
+  in
+  {
+    to_raw = (fun v -> w.to_raw (v.html_key, v.html_begin, v.html_end)) ;
+    of_raw =
+      (fun r -> let (k,b,e) = w.of_raw r in
+       { html_key = k ; html_begin = b ; html_end = e }
+      ) ;
+  }
 
-  let (t : html_binding option_class) =
-    define_option_class "html_binding" value_to_hb hb_to_value
-end
+class htmlbinding_cp =
+  [html_binding] Config_file.option_cp htmlbinding_cp_wrapper
diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml
index 17e371f5..57939266 100644
--- a/ide/utils/okey.ml
+++ b/ide/utils/okey.ml
@@ -1,33 +1,34 @@
-(**************************************************************************)
-(*                   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                                *)
-(**************************************************************************)
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
 
 type modifier = Gdk.Tags.modifier
 
 type handler = {
     cond : (unit -> bool) ;
     cback : (unit -> unit) ;
-  } 
+  }
 
 type handler_spec = int * int * Gdk.keysym
       (** mods * mask * key *)
@@ -49,9 +50,9 @@ let int_of_modifier = function
 
 let print_modifier l =
   List.iter
-    (fun m -> 
+    (fun m ->
       print_string
-	(((function 
+	(((function
 	    `SHIFT -> "SHIFT"
 	  | `LOCK -> "LOCK"
 	  | `CONTROL -> "CONTROL"
@@ -69,11 +70,11 @@ let print_modifier l =
     )
     l;
   print_newline ()
-  
+
 let int_of_modifiers l =
   List.fold_left (fun acc -> fun m -> acc + (int_of_modifier m)) 0 l
 
-module H = 
+module H =
   struct
     type t = handler_spec * handler
     let equal (m,k) (mods, mask, key) =
@@ -85,7 +86,7 @@ module H =
     let find_handlers mods key l =
       List.map snd
         (List.filter
-	   (fun ((m,ma,k),_) -> equal (mods,key) (m,ma,k)) 
+	   (fun ((m,ma,k),_) -> equal (mods,key) (m,ma,k))
 	   l
 	)
 
@@ -97,23 +98,25 @@ let key_press w ev =
   let key = GdkEvent.Key.keyval ev in
   let modifiers = GdkEvent.Key.state ev in
   try
-    let (r : H.t list ref) = Hashtbl.find table w#get_oid in
+    let (r : H.t list ref) = Hashtbl.find table (Oo.id w) in
     let l = H.find_handlers (int_of_modifiers modifiers) key !r in
-    let b = ref true in
-    List.iter
-      (fun h ->
-	if h.cond () then
-	  (h.cback () ; b := false)
-	else
-	  ()
-      )
-      l;
-    !b
+    match l with
+      [] -> false
+    | _ ->
+	List.iter
+	  (fun h ->
+	    if h.cond () then
+	      try h.cback ()
+	      with e -> prerr_endline (Printexc.to_string e)
+	    else ()
+	  )
+	  l;
+	true
   with
     Not_found ->
-      true
+      false
 
-let associate_key_press w = 
+let associate_key_press w =
   ignore ((w#event#connect#key_press ~callback: (key_press w)) : GtkSignal.id)
 
 let default_modifiers = ref ([] : modifier list)
@@ -122,24 +125,25 @@ let default_mask = ref ([`MOD2 ; `MOD3 ; `MOD4 ; `MOD5 ; `LOCK] : modifier list)
 let set_default_modifiers l = default_modifiers := l
 let set_default_mask l = default_mask := l
 
-let remove_widget  (w : < event : GObj.event_ops ; get_oid : int ; ..>) () =
-  try 
-    let r = Hashtbl.find table w#get_oid in
+let remove_widget  (w : < event : GObj.event_ops ; ..>) () =
+  try
+    let r = Hashtbl.find table (Oo.id w) in
     r := []
-  with 
+  with
     Not_found ->
       ()
 
 let add1 ?(remove=false) w
-    ?(cond=(fun () -> true)) 
+    ?(cond=(fun () -> true))
     ?(mods= !default_modifiers)
     ?(mask= !default_mask)
     k callback =
+
   let r =
-    try Hashtbl.find table w#get_oid
-    with Not_found -> 
+    try Hashtbl.find table (Oo.id w)
+    with Not_found ->
       let r = ref [] in
-      Hashtbl.add table w#get_oid r;
+      Hashtbl.add table (Oo.id w) r;
       ignore (w#connect#destroy ~callback: (remove_widget w));
       associate_key_press w;
       r
@@ -147,7 +151,7 @@ let add1 ?(remove=false) w
   let n_mods = int_of_modifiers mods in
   let n_mask = lnot (int_of_modifiers mask) in
   let new_h = { cond = cond ; cback = callback } in
-  if remove then 
+  if remove then
     (
      let l = H.filter_with_mask n_mods n_mask k !r in
      r := ((n_mods, n_mask, k), new_h) :: l
@@ -156,30 +160,29 @@ let add1 ?(remove=false) w
     r := ((n_mods, n_mask, k), new_h) :: !r
 
 let add w
-    ?(cond=(fun () -> true)) 
+    ?(cond=(fun () -> true))
     ?(mods= !default_modifiers)
     ?(mask= !default_mask)
     k callback =
   add1 w ~cond ~mods ~mask k callback
 
 let add_list w
-    ?(cond=(fun () -> true)) 
+    ?(cond=(fun () -> true))
     ?(mods= !default_modifiers)
     ?(mask= !default_mask)
     k_list callback =
   List.iter (fun k -> add w ~cond ~mods ~mask k callback) k_list
 
 let set w
-    ?(cond=(fun () -> true)) 
+    ?(cond=(fun () -> true))
     ?(mods= !default_modifiers)
     ?(mask= !default_mask)
     k callback =
   add1 ~remove: true w ~cond ~mods ~mask k callback
 
 let set_list w
-    ?(cond=(fun () -> true)) 
+    ?(cond=(fun () -> true))
     ?(mods= !default_modifiers)
     ?(mask= !default_mask)
     k_list callback =
   List.iter (fun k -> set w ~cond ~mods ~mask k callback) k_list
-
diff --git a/ide/utils/okey.mli b/ide/utils/okey.mli
index a0effe72..c8d48389 100644
--- a/ide/utils/okey.mli
+++ b/ide/utils/okey.mli
@@ -1,26 +1,27 @@
-(**************************************************************************)
-(*                   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                                *)
-(**************************************************************************)
+(*********************************************************************************)
+(*                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                                          *)
+(*                                                                               *)
+(*********************************************************************************)
 
 (** Okey interface.