coqide: load/save file encoding support/

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

12 files changed, 516 insertions, 379 deletions

diff --git a/.depend b/.depend
index eeb3134df..c3994fc76 100644
--- a/.depend
+++ b/.depend
@@ -505,12 +505,12 @@ ide/coq_tactics.cmo: ide/coq_tactics.cmi
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
 ide/coqide.cmo: ide/command_windows.cmi ide/coq.cmi ide/coq_commands.cmo \
     ide/find_phrase.cmo ide/highlight.cmo ide/ideutils.cmi proofs/pfedit.cmi \
-    ide/preferences.cmi ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo \
-    ide/coqide.cmi 
+    ide/preferences.cmi ide/undo.cmi ide/utf8_convert.cmo lib/util.cmi \
+    toplevel/vernacexpr.cmo ide/coqide.cmi 
 ide/coqide.cmx: ide/command_windows.cmx ide/coq.cmx ide/coq_commands.cmx \
     ide/find_phrase.cmx ide/highlight.cmx ide/ideutils.cmx proofs/pfedit.cmx \
-    ide/preferences.cmx ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx \
-    ide/coqide.cmi 
+    ide/preferences.cmx ide/undo.cmx ide/utf8_convert.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx ide/coqide.cmi 
 ide/find_phrase.cmo: ide/ideutils.cmi 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmi 
diff --git a/.depend.newcoq b/.depend.newcoq
index 823877947..385da3b20 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -53,19 +53,18 @@ newtheories/Reals/RiemannInt_SF.vo: newtheories/Reals/RiemannInt_SF.v newtheorie
 newtheories/Reals/RiemannInt.vo: newtheories/Reals/RiemannInt.v newtheories/Reals/Rfunctions.vo newtheories/Reals/SeqSeries.vo newtheories/Reals/Ranalysis.vo newtheories/Reals/Rbase.vo newtheories/Reals/RiemannInt_SF.vo newtheories/Logic/Classical_Prop.vo newtheories/Logic/Classical_Pred_Type.vo newtheories/Arith/Max.vo
 newtheories/Reals/Integration.vo: newtheories/Reals/Integration.v newtheories/Reals/NewtonInt.vo newtheories/Reals/RiemannInt_SF.vo newtheories/Reals/RiemannInt.vo
 newtheories/Reals/Reals.vo: newtheories/Reals/Reals.v newtheories/Reals/Rbase.vo newtheories/Reals/Rfunctions.vo newtheories/Reals/SeqSeries.vo newtheories/Reals/Rtrigo.vo newtheories/Reals/Ranalysis.vo newtheories/Reals/Integration.vo
-newtheories/Init/Notations.vo: newtheories/Init/Notations.v
 newtheories/Init/Datatypes.vo: newtheories/Init/Datatypes.v
 newtheories/Init/DatatypesSyntax.vo: newtheories/Init/DatatypesSyntax.v
 newtheories/Init/Peano.vo: newtheories/Init/Peano.v newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Datatypes.vo
 newtheories/Init/PeanoSyntax.vo: newtheories/Init/PeanoSyntax.v newtheories/Init/Datatypes.vo newtheories/Init/Peano.vo
-newtheories/Init/Logic.vo: newtheories/Init/Logic.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo
+newtheories/Init/Logic.vo: newtheories/Init/Logic.v newtheories/Init/Datatypes.vo
 newtheories/Init/Specif.vo: newtheories/Init/Specif.v newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo
 newtheories/Init/LogicSyntax.vo: newtheories/Init/LogicSyntax.v newtheories/Init/Logic.vo
 newtheories/Init/SpecifSyntax.vo: newtheories/Init/SpecifSyntax.v newtheories/Init/Datatypes.vo newtheories/Init/Specif.vo
 newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo
 newtheories/Init/Wf.vo: newtheories/Init/Wf.v newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo
 newtheories/Init/Logic_TypeSyntax.vo: newtheories/Init/Logic_TypeSyntax.v newtheories/Init/Logic_Type.vo
-newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/DatatypesSyntax.vo newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Specif.vo newtheories/Init/SpecifSyntax.vo newtheories/Init/Peano.vo newtheories/Init/PeanoSyntax.vo newtheories/Init/Wf.vo
+newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Datatypes.vo newtheories/Init/DatatypesSyntax.vo newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Specif.vo newtheories/Init/SpecifSyntax.vo newtheories/Init/Peano.vo newtheories/Init/PeanoSyntax.vo newtheories/Init/Wf.vo
 newtheories/Logic/Hurkens.vo: newtheories/Logic/Hurkens.v
 newtheories/Logic/ProofIrrelevance.vo: newtheories/Logic/ProofIrrelevance.v newtheories/Logic/Hurkens.vo
 newtheories/Logic/Classical.vo: newtheories/Logic/Classical.v newtheories/Logic/Classical_Prop.vo newtheories/Logic/Classical_Pred_Set.vo
@@ -90,7 +89,7 @@ newtheories/Arith/Compare_dec.vo: newtheories/Arith/Compare_dec.v newtheories/Ar
 newtheories/Arith/Min.vo: newtheories/Arith/Min.v newtheories/Arith/Arith.vo
 newtheories/Arith/Div2.vo: newtheories/Arith/Div2.v newtheories/Arith/Lt.vo newtheories/Arith/Plus.vo newtheories/Arith/Compare_dec.vo newtheories/Arith/Even.vo
 newtheories/Arith/Minus.vo: newtheories/Arith/Minus.v newtheories/Arith/Lt.vo newtheories/Arith/Le.vo
-newtheories/Arith/Mult.vo: newtheories/Arith/Mult.v newtheories/Arith/Plus.vo newtheories/Arith/Minus.vo newtheories/Arith/Lt.vo
+newtheories/Arith/Mult.vo: newtheories/Arith/Mult.v newtheories/Arith/Plus.vo newtheories/Arith/Minus.vo newtheories/Arith/Lt.vo newtheories/Arith/Le.vo
 newtheories/Arith/Even.vo: newtheories/Arith/Even.v
 newtheories/Arith/EqNat.vo: newtheories/Arith/EqNat.v
 newtheories/Arith/Peano_dec.vo: newtheories/Arith/Peano_dec.v newtheories/Logic/Decidable.vo
@@ -99,7 +98,7 @@ newtheories/Arith/Plus.vo: newtheories/Arith/Plus.v newtheories/Arith/Le.vo newt
 newtheories/Arith/Wf_nat.vo: newtheories/Arith/Wf_nat.v newtheories/Arith/Lt.vo
 newtheories/Arith/Max.vo: newtheories/Arith/Max.v newtheories/Arith/Arith.vo
 newtheories/Arith/Bool_nat.vo: newtheories/Arith/Bool_nat.v newtheories/Arith/Compare_dec.vo newtheories/Arith/Peano_dec.vo newtheories/Bool/Sumbool.vo
-newtheories/Arith/Factorial.vo: newtheories/Arith/Factorial.v newtheories/Arith/Plus.vo newtheories/Arith/Lt.vo
+newtheories/Arith/Factorial.vo: newtheories/Arith/Factorial.v newtheories/Arith/Plus.vo newtheories/Arith/Mult.vo newtheories/Arith/Lt.vo
 newtheories/Bool/Bool.vo: newtheories/Bool/Bool.v
 newtheories/Bool/IfProp.vo: newtheories/Bool/IfProp.v newtheories/Bool/Bool.vo
 newtheories/Bool/Zerob.vo: newtheories/Bool/Zerob.v newtheories/Arith/Arith.vo newtheories/Bool/Bool.vo
diff --git a/Makefile b/Makefile
index 1dbb7ac47..36545e5bd 100644
--- a/Makefile
+++ b/Makefile
@@ -387,7 +387,7 @@ COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \
 	  ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \
 	  ide/utils/configwin.cmo \
 	  ide/utils/editable_cells.cmo ide/config_parser.cmo \
-	  ide/config_lexer.cmo ide/preferences.cmo \
+	  ide/config_lexer.cmo ide/utf8_convert.cmo ide/preferences.cmo \
 	  ide/ideutils.cmo ide/undo.cmo \
 	  ide/find_phrase.cmo \
           ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \
@@ -397,6 +397,7 @@ COQIDECMX=$(COQIDECMO:.cmo=.cmx)
 COQIDEFLAGS=-thread -I +lablgtk2
 beforedepend:: ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml
 beforedepend:: ide/config_parser.mli ide/config_parser.ml
+beforedepend:: ide/utf8_convert.ml
 
 FULLIDELIB=$(FULLCOQLIB)/ide
 IDEFILES=ide/coq.png ide/.coqide-gtk2rc
diff --git a/ide/FAQ b/ide/FAQ
index 53b34d7ea..2dcbd1dfd 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -55,8 +55,16 @@ R6) Use
 	coqmktop -ide -opt m1.cmx...mi.cmx
 
 Q7) How to customize the shortcuts for menus?
-R6) Two solutions are offered:
+R7) Two solutions are offered:
   - Edit $HOME/.coqide.keys by hand
   - Add "gtk-can-change-accels = 1" in your .coqiderc.gtk2 file. Then
     from CoqIde, you may select a menu entry and press the desired 
     shortcut. Do not forget to save your preferences.
+
+Q8) What encoding should I use? What is this \x{iiii} in my file?
+R8) The encoding option is related to the way files are saved. Keep it as UTF-8 until
+    it becomes important for you to exchange files with non UTF-8 aware applications.
+    
+    If you choose something else than UTF-8, then missing characters will be encoded by
+	\x{....} or \x{........} where the dot is a digit. The number between braces is 
+    the hexadecimal UNICODE index for the missing character.
diff --git a/ide/coq.ml b/ide/coq.ml
index 01a1c4c13..cccd91114 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -57,7 +57,7 @@ let is_in_coq_lib dir =
 			Coq_config.coqlib 
 			(Filename.concat "theories" s) 
 	   in
-	   prerr_endline (" Comparing to : "^fdir);
+	   prerr_endline (" Comparing to: "^fdir);
 	   let fstat = Unix.stat fdir in 
 	   (fstat.Unix.st_dev = stat.Unix.st_dev) &&
 	   (fstat.Unix.st_ino = stat.Unix.st_ino) && 
@@ -140,7 +140,6 @@ let interp_last last =
     raise e
 
 
-(* type hyp = (identifier * constr option * constr) * string*)
 type hyp = env * evar_map *
            ((identifier * string) * constr option * constr) * 
            (string * string)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 698987329..85e412df6 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -15,7 +15,7 @@ open Ideutils
 open Format
 
 let out_some s = match s with 
-  | None -> failwith "Internal error in out_some." | Some f -> f
+  | None -> failwith "Internal error in out_some" | Some f -> f
 
 let cb_ = ref None
 let cb () = out_some !cb_
@@ -204,7 +204,7 @@ let crash_save i =
        (let filename = match av#filename with 
 	 | None -> 
 	     incr count; 
-	     "Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide"
+	     "Unamed_coqscript_"^(string_of_int !count)^".crashcoqide"
 	 | Some f -> f^".crashcoqide"
        in
        try 
@@ -680,14 +680,14 @@ object(self)
   method recenter_insert = 
     (* BUG : to investigate further: 
        FIXED : Never call  GMain.* in thread !
-       PLUS : GTK BUG ??? Cannot be called from a thread...*)
-    try 
-      ignore (GtkThread.sync (input_view#scroll_to_mark 
-				~use_align:false
-				~yalign:0.75
-				~within_margin:0.25)
-		`INSERT) 
-    with _ -> prerr_endline "Could not recenter ERROR ignored"
+       PLUS : GTK BUG ??? Cannot be called from a thread...
+       ADDITION: using sync instead of async causes deadlock...*)
+    ignore (GtkThread.async (
+	      input_view#scroll_to_mark 
+			       ~use_align:false
+			       ~yalign:0.75
+			       ~within_margin:0.25)
+	      `INSERT)
 
   method show_goals = 
     try
@@ -732,112 +732,117 @@ object(self)
       with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
 	
 
+  val mutable full_goal_done = false
+
   method show_goals_full = 
-    begin
-      try
-	proof_view#buffer#set_text "";
-	let s = Coq.get_current_goals () in
-	let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light green"]
-	in
-	match s with 
-	| [] -> proof_buffer#insert (Coq.print_no_goal ())
-	| (hyps,concl)::r -> 
-	    let goal_nb = List.length s in
-	    proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" 
-				   goal_nb
-				   (if goal_nb<=1 then "" else "s"));
-	    let coq_menu commands = 
-	      let tag = proof_buffer#create_tag []
-	      in 
-	      ignore
-		(tag#connect#event ~callback:
-		   (fun ~origin ev it ->
-		      match GdkEvent.get_type ev with 
-		      | `BUTTON_PRESS -> 
-			  let ev = (GdkEvent.Button.cast ev) in
-			  if (GdkEvent.Button.button ev) = 3
-			  then begin 
-			    let loc_menu = GMenu.menu () in
-			    let factory = new GMenu.factory loc_menu in
-			    let add_coq_command (cp,ip) = 
-			      ignore 
-				(factory#add_item cp 
-				   ~callback:
-				   (fun () -> ignore
-				      (self#insert_this_phrase_on_success 
-					 true
-					 true 
-					 false 
-					 (ip^"\n") 
-					 (ip^"\n"))
-				   )
-				)
-			    in
-			    List.iter add_coq_command commands;
-			    loc_menu#popup 
-			      ~button:3
-			      ~time:(GdkEvent.Button.time ev);
-			  end
-		      | `MOTION_NOTIFY -> 
-			  proof_buffer#remove_tag
-			  ~start:proof_buffer#start_iter
-			  ~stop:proof_buffer#end_iter
-			  last_shown_area;
-			  prerr_endline "Before find_tag_limits";
-			  
-			  let s,e = find_tag_limits tag 
-				      (new GText.iter it) 
-			  in
-			  prerr_endline "After find_tag_limits";
-			  proof_buffer#apply_tag 
-			    ~start:s 
-			    ~stop:e 
+    if not full_goal_done then
+      begin
+	try
+	  proof_view#buffer#set_text "";
+	  let s = Coq.get_current_goals () in
+	  let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light green"]
+	  in
+	  match s with 
+	  | [] -> proof_buffer#insert (Coq.print_no_goal ())
+	  | (hyps,concl)::r -> 
+	      let goal_nb = List.length s in
+	      proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" 
+				     goal_nb
+				     (if goal_nb<=1 then "" else "s"));
+	      let coq_menu commands = 
+		let tag = proof_buffer#create_tag []
+		in 
+		ignore
+		  (tag#connect#event ~callback:
+		     (fun ~origin ev it ->
+			match GdkEvent.get_type ev with 
+			| `BUTTON_PRESS -> 
+			    let ev = (GdkEvent.Button.cast ev) in
+			    if (GdkEvent.Button.button ev) = 3
+			    then begin 
+			      let loc_menu = GMenu.menu () in
+			      let factory = new GMenu.factory loc_menu in
+			      let add_coq_command (cp,ip) = 
+				ignore 
+				  (factory#add_item cp 
+				     ~callback:
+				     (fun () -> ignore
+					(self#insert_this_phrase_on_success 
+					   true
+					   true 
+					   false 
+					   (ip^"\n") 
+					   (ip^"\n"))
+				     )
+				  )
+			      in
+			      List.iter add_coq_command commands;
+			      loc_menu#popup 
+				~button:3
+				~time:(GdkEvent.Button.time ev);
+			    end
+			| `MOTION_NOTIFY -> 
+			    proof_buffer#remove_tag
+			    ~start:proof_buffer#start_iter
+			    ~stop:proof_buffer#end_iter
 			    last_shown_area;
-			  
-			  prerr_endline "Applied tag";
-			  ()
-		      | _ -> ())
-		);
-	      tag
-	    in
-	    List.iter
-	      (fun ((_,_,_,(s,_)) as hyp) -> 
-		 let tag = coq_menu (hyp_menu hyp) in
-		 proof_buffer#insert ~tags:[tag] (s^"\n"))
-	      hyps;
-	    proof_buffer#insert 
-	      (String.make 38 '_' ^"(1/"^
-	       (string_of_int goal_nb)^
-	       ")\n") 
-	    ;
-	    let tag = coq_menu (concl_menu concl) in
-	    let _,_,_,sconcl = concl in
-	    proof_buffer#insert ~tags:[tag] sconcl;
-	    proof_buffer#insert "\n";
-	    let my_mark = `NAME "end_of_conclusion" in
-	    proof_buffer#move_mark
-	      ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
-	    proof_buffer#insert "\n\n";
-	    let i = ref 1 in
-	    List.iter 
-	      (function (_,(_,_,_,concl)) -> 
-		 incr i;
-		 proof_buffer#insert 
-		   (String.make 38 '_' ^"("^
-		    (string_of_int !i)^
-		    "/"^
-		    (string_of_int goal_nb)^
-		    ")\n");
-		 proof_buffer#insert concl;
-		 proof_buffer#insert "\n\n";
-	      )
-	      r;
-	    ignore (proof_view#scroll_to_mark my_mark) ;
-	with e -> prerr_endline (Printexc.to_string e)
-    end
-
+			    prerr_endline "Before find_tag_limits";
+			    
+			    let s,e = find_tag_limits tag 
+					(new GText.iter it) 
+			    in
+			    prerr_endline "After find_tag_limits";
+			    proof_buffer#apply_tag 
+			      ~start:s 
+			      ~stop:e 
+			      last_shown_area;
+			    
+			    prerr_endline "Applied tag";
+			    ()
+			| _ -> ())
+		  );
+		tag
+	      in
+	      List.iter
+		(fun ((_,_,_,(s,_)) as hyp) -> 
+		   let tag = coq_menu (hyp_menu hyp) in
+		   proof_buffer#insert ~tags:[tag] (s^"\n"))
+		hyps;
+	      proof_buffer#insert 
+		(String.make 38 '_' ^"(1/"^
+		 (string_of_int goal_nb)^
+		 ")\n") 
+	      ;
+	      let tag = coq_menu (concl_menu concl) in
+	      let _,_,_,sconcl = concl in
+	      proof_buffer#insert ~tags:[tag] sconcl;
+	      proof_buffer#insert "\n";
+	      let my_mark = `NAME "end_of_conclusion" in
+	      proof_buffer#move_mark
+		~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
+	      proof_buffer#insert "\n\n";
+	      let i = ref 1 in
+	      List.iter 
+		(function (_,(_,_,_,concl)) -> 
+		   incr i;
+		   proof_buffer#insert 
+		     (String.make 38 '_' ^"("^
+		      (string_of_int !i)^
+		      "/"^
+		      (string_of_int goal_nb)^
+		      ")\n");
+		   proof_buffer#insert concl;
+		   proof_buffer#insert "\n\n";
+		)
+		r;
+	      ignore (proof_view#scroll_to_mark my_mark) ;
+	      full_goal_done <- true;
+	  with e -> prerr_endline (Printexc.to_string e)
+      end
+      
   method send_to_coq phrase show_output show_error localize =
     try 
+      full_goal_done <- false;
       prerr_endline "Send_to_coq starting now";
       let r = Some (Coq.interp phrase) in
       let msg = read_stdout () in 
@@ -1534,8 +1539,8 @@ let main files =
 	(function 
 	   | {analyzed_view=Some av} -> 
 	       (match av#filename with 
-		  | None -> false 
-		  | Some fn -> f=fn)
+		| None -> false 
+		| Some fn -> f=fn)
 	   | _ -> false) 
 	!input_views;
       let b = Buffer.create 1024 in
@@ -1565,15 +1570,15 @@ let main files =
       input_buffer#set_modified false;
       av#view#clear_undo
     with       
-      | Vector.Found i -> set_current_view i
-      | e -> !flash_info ("Load failed: "^(Printexc.to_string e))
+    | Vector.Found i -> set_current_view i
+    | e -> !flash_info ("Load failed: "^(Printexc.to_string e))
   in
   let load_m = file_factory#add_item "_Open/Create" 
 		 ~key:GdkKeysyms._O in
   let load_f () = 	  
-    match  select_file ~title:"Load file" () with 
-      | None -> ()
-      | (Some f) as fn -> load f
+    match select_file ~title:"Load file" () with 
+    | None -> ()
+    | (Some f) as fn -> load f
   in
   ignore (load_m#connect#activate (load_f));
 
@@ -1584,25 +1589,25 @@ let main files =
     let current = get_current_view () in
     try
       (match (out_some current.analyzed_view)#filename with 
-	 | None ->
-	     begin match GToolbox.select_file ~title:"Save file" ()
-	     with
-	       | None -> ()
-	       | Some f -> 
-		   if (out_some current.analyzed_view)#save_as f then begin
-		     set_current_tab_label (Filename.basename f);
-		     !flash_info "Saved"
-		   end
-		   else !flash_info "Save Failed"
-	     end
-	 | Some f -> 
-	     if (out_some current.analyzed_view)#save f then 
-	       !flash_info "Saved"
-	     else !flash_info "Save Failed"
-	       
+       | None ->
+	   begin match GToolbox.select_file ~title:"Save file" ()
+	   with
+	   | None -> ()
+	   | Some f -> 
+	       if (out_some current.analyzed_view)#save_as f then begin
+		 set_current_tab_label (Filename.basename f);
+		 !flash_info "Saved"
+	       end
+	       else !flash_info "Save Failed"
+	   end
+       | Some f -> 
+	   if (out_some current.analyzed_view)#save f then 
+	     !flash_info "Saved"
+	   else !flash_info "Save Failed"
+	     
       )
     with 
-      | e -> !flash_info "Save failed"
+    | e -> !flash_info "Save failed"
   in   
   ignore (save_m#connect#activate save_f);
 
@@ -1612,30 +1617,30 @@ let main files =
   let saveas_f () = 
     let current = get_current_view () in
     try (match (out_some current.analyzed_view)#filename with 
-	   | None -> 
-	       begin match GToolbox.select_file ~title:"Save file as" ()
-	       with
-		 | None -> ()
-		 | Some f -> 
-		     if (out_some current.analyzed_view)#save_as f then begin
-		       set_current_tab_label (Filename.basename f);
-		       !flash_info "Saved"
-		     end
-		     else !flash_info "Save Failed"
-	       end
-	   | Some f -> 
-	       begin match GToolbox.select_file 
-		 ~dir:(ref (Filename.dirname f)) 
-		 ~filename:(Filename.basename f)
-		 ~title:"Save file as" ()
-	       with
-		 | None -> ()
-		 | Some f -> 
-		     if (out_some current.analyzed_view)#save_as f then begin
-		       set_current_tab_label (Filename.basename f);
-		       !flash_info "Saved"
-		     end else !flash_info "Save Failed"
-	       end);
+	 | None -> 
+	     begin match GToolbox.select_file ~title:"Save file as" ()
+	     with
+	     | None -> ()
+	     | Some f -> 
+		 if (out_some current.analyzed_view)#save_as f then begin
+		   set_current_tab_label (Filename.basename f);
+		   !flash_info "Saved"
+		 end
+		 else !flash_info "Save Failed"
+	     end
+	 | Some f -> 
+	     begin match GToolbox.select_file 
+	       ~dir:(ref (Filename.dirname f)) 
+	       ~filename:(Filename.basename f)
+	       ~title:"Save file as" ()
+	     with
+	     | None -> ()
+	     | Some f -> 
+		 if (out_some current.analyzed_view)#save_as f then begin
+		   set_current_tab_label (Filename.basename f);
+		   !flash_info "Saved"
+		 end else !flash_info "Save Failed"
+	     end);
     with e -> !flash_info "Save Failed"
   in   
   ignore (saveas_m#connect#activate saveas_f);
@@ -1648,9 +1653,9 @@ let main files =
       (function 
 	 | {view = view ; analyzed_view = Some av} as full -> 
 	     begin match av#filename with 
-	       | None -> ()
-	       | Some f ->
-		   ignore (av#save f)
+	     | None -> ()
+	     | Some f ->
+		 ignore (av#save f)
 	     end
 	 | _ -> ()
       )  input_views
@@ -1672,12 +1677,12 @@ let main files =
 	   {view = view ; analyzed_view = Some av} as full -> 
 	     (try 
 		match av#filename,av#stats with 
-		  | Some f,Some stats -> 
-		      let new_stats = Unix.stat f in
-		      if new_stats.Unix.st_mtime > stats.Unix.st_mtime 
-		      then av#revert
-		  | Some _, None -> av#revert
-		  | _ -> ()
+		| Some f,Some stats -> 
+		    let new_stats = Unix.stat f in
+		    if new_stats.Unix.st_mtime > stats.Unix.st_mtime 
+		    then av#revert
+		| Some _, None -> av#revert
+		| _ -> ()
 		with _ -> av#revert)
 	 | _ -> ()
       )  input_views
@@ -1699,16 +1704,16 @@ let main files =
     let v = get_current_view () in
     let av = out_some v.analyzed_view in
     match av#filename with
-      | None -> 
-	  !flash_info "Cannot print: this buffer has no name"
-      | Some f ->
-	  let cmd = 
-	    "cd " ^ Filename.dirname f ^ "; " ^
-	    !current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^ 
-	    " | " ^ !current.cmd_print
-	  in
-	  let c = Sys.command cmd in
-	  !flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
+    | None -> 
+	!flash_info "Cannot print: this buffer has no name"
+    | Some f ->
+	let cmd = 
+	  "cd " ^ Filename.dirname f ^ "; " ^
+	  !current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^ 
+	  " | " ^ !current.cmd_print
+	in
+	let c = Sys.command cmd in
+	!flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
   in
   let print_m = file_factory#add_item "_Print" ~callback:print_f in
 
@@ -1717,23 +1722,23 @@ let main files =
     let v = get_current_view () in
     let av = out_some v.analyzed_view in
     match av#filename with
-      | None -> 
-	  !flash_info "Cannot print: this buffer has no name"
-      | Some f ->
-	  let basef = Filename.basename f in
-	  let output = 
-	    let basef_we = try Filename.chop_extension basef with _ -> basef in
-	    match kind with
-	      | "latex" -> basef_we ^ ".tex"
-	      | "dvi" | "ps" | "html" -> basef_we ^ "." ^ kind
-	      | _ -> assert false
-	  in
-	  let cmd = 
-	    "cd " ^ Filename.dirname f ^ "; " ^
-	    !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef
-	  in
-	  let c = Sys.command cmd in
-	  !flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
+    | None -> 
+	!flash_info "Cannot print: this buffer has no name"
+    | Some f ->
+	let basef = Filename.basename f in
+	let output = 
+	  let basef_we = try Filename.chop_extension basef with _ -> basef in
+	  match kind with
+	  | "latex" -> basef_we ^ ".tex"
+	  | "dvi" | "ps" | "html" -> basef_we ^ "." ^ kind
+	  | _ -> assert false
+	in
+	let cmd = 
+	  "cd " ^ Filename.dirname f ^ "; " ^
+	  !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef
+	in
+	let c = Sys.command cmd in
+	!flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
   in
   let file_export_m =  file_factory#add_submenu "E_xport to" in
 
@@ -1778,8 +1783,8 @@ let main files =
 	       "There are unsaved buffers"
 	    )
       with 1 -> saveall_f () ; exit 0
-	| 2 -> exit 0
-	| _ -> ()
+      | 2 -> exit 0
+      | _ -> ()
     else exit 0
   in
   let quit_m = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q 
@@ -1869,7 +1874,7 @@ let main files =
   let do_or_activate f = do_if_not_computing (do_or_activate f) in
 
   let add_to_menu_toolbar text ~tooltip ~key ~callback icon = 
-     ignore (navigation_factory#add_item text ~key ~callback);
+    ignore (navigation_factory#add_item text ~key ~callback);
     ignore (toolbar#insert_button
 	      ~tooltip
 	      ~text:tooltip
@@ -1977,15 +1982,15 @@ let main files =
 
 
   ignore (toolbar#insert_button
-	    ~tooltip:"Proof Wizzard"
-	    ~text:"Wizzard"
+	    ~tooltip:"Proof Wizard"
+	    ~text:"Wizard"
 	    ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_INFO)
 	    ~callback:(do_if_active (fun a -> a#insert_commands 
 				       !current.automatic_tactics
 				    ))
 	    ());
 
-  ignore (tactics_factory#add_item "<Proof _Wizzard>"
+  ignore (tactics_factory#add_item "<Proof _Wizard>"
 	    ~key:GdkKeysyms._dollar
 	    ~callback:(do_if_active (fun a -> a#insert_commands 
 				       !current.automatic_tactics
@@ -2028,40 +2033,40 @@ let main files =
     ("_Inductive __", "Inductive ident : :=\n  | : .\n",
      14, 5, Some GdkKeysyms._I);
   add_complex_template("_Scheme __",
-"Scheme new_scheme := Induction for _ Sort _
+		       "Scheme new_scheme := Induction for _ Sort _
 with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 
-(* Template for Cases *)
+  (* Template for Cases *)
   let callback = (fun () -> 
-			 let w = get_current_word () in
-			 try 
-			   let cases = Coq.make_cases w
-			   in
-			   let print c = function
-			     | [x] -> fprintf c "  | %s => _@\n" x
-			     | x::l -> fprintf c "  | (%s%a) => _@\n" x 
-				 (print_list (fun c s -> fprintf c " %s" s)) l
-			     | [] -> assert false
-			   in
-			   let b = Buffer.create 1024 in
-			   let fmt = formatter_of_buffer b in
-			   fprintf fmt "@[Cases var of@\n%aend@]@."
-			     (print_list print) cases;
-			   let s = Buffer.contents b in
-			   prerr_endline s;
-			   let {view = view } = get_current_view () in
-			   ignore (view#buffer#delete_selection ());
-			   let m = view#buffer#create_mark 
-				     (view#buffer#get_iter `INSERT)
-			   in
-			   if view#buffer#insert_interactive s then 
-			     let i = view#buffer#get_iter (`MARK m) in
-			     let _ = i#nocopy#forward_chars 9 in
-			     view#buffer#place_cursor i;
-			     view#buffer#move_mark ~where:(i#backward_chars 3)
-			       `SEL_BOUND 
-			 with Not_found -> !flash_info "Not an inductive type"
-		      )
+		    let w = get_current_word () in
+		    try 
+		      let cases = Coq.make_cases w
+		      in
+		      let print c = function
+			| [x] -> fprintf c "  | %s => _@\n" x
+			| x::l -> fprintf c "  | (%s%a) => _@\n" x 
+			    (print_list (fun c s -> fprintf c " %s" s)) l
+			| [] -> assert false
+		      in
+		      let b = Buffer.create 1024 in
+		      let fmt = formatter_of_buffer b in
+		      fprintf fmt "@[Cases var of@\n%aend@]@."
+			(print_list print) cases;
+		      let s = Buffer.contents b in
+		      prerr_endline s;
+		      let {view = view } = get_current_view () in
+		      ignore (view#buffer#delete_selection ());
+		      let m = view#buffer#create_mark 
+				(view#buffer#get_iter `INSERT)
+		      in
+		      if view#buffer#insert_interactive s then 
+			let i = view#buffer#get_iter (`MARK m) in
+			let _ = i#nocopy#forward_chars 9 in
+			view#buffer#place_cursor i;
+			view#buffer#move_mark ~where:(i#backward_chars 3)
+			  `SEL_BOUND 
+		    with Not_found -> !flash_info "Not an inductive type"
+		 )
   in
   ignore (templates_factory#add_item "Cases ..."
 	    ~key:GdkKeysyms._C
@@ -2092,22 +2097,22 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   List.iter 
     (fun l -> 
        match l with 
-	 |[s] -> add_simple_template templates_factory ("_"^s, s^" ") 
-	 | [] -> ()
-	 | s::r -> 
-	     let a = "_@..." in
-	     a.[1] <- s.[0];
-	     let f = templates_factory#add_submenu a in 
-	     let ff = new GMenu.factory f ~accel_group in
-	     List.iter 
-	       (fun x -> 
-		  add_simple_template 
-		  ff 
-		  ((String.sub x 0 1)^
-		   "_"^
-		   (String.sub x 1 (String.length x - 1)),
-		   x^" "))
-	       l
+       |[s] -> add_simple_template templates_factory ("_"^s, s^" ") 
+       | [] -> ()
+       | s::r -> 
+	   let a = "_@..." in
+	   a.[1] <- s.[0];
+	   let f = templates_factory#add_submenu a in 
+	   let ff = new GMenu.factory f ~accel_group in
+	   List.iter 
+	     (fun x -> 
+		add_simple_template 
+		ff 
+		((String.sub x 0 1)^
+		 "_"^
+		 (String.sub x 1 (String.length x - 1)),
+		 x^" "))
+	     l
     ) 
     Coq_commands.commands;
   
@@ -2161,16 +2166,16 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
     let v = get_active_view () in
     let av = out_some v.analyzed_view in
     match av#filename with
-      | None -> 
-	  !flash_info "Active buffer has no name"
-      | Some f ->
-	  let c = Sys.command (!current.cmd_coqc ^ " " ^ f) in
-	  if c = 0 then
-	    !flash_info (f ^ " successfully compiled")
-	  else begin
-	    !flash_info (f ^ " failed to compile");
-	    av#process_until_end_or_error
-	  end
+    | None -> 
+	!flash_info "Active buffer has no name"
+    | Some f ->
+	let c = Sys.command (!current.cmd_coqc ^ " " ^ f) in
+	if c = 0 then
+	  !flash_info (f ^ " successfully compiled")
+	else begin
+	  !flash_info (f ^ " failed to compile");
+	  av#process_until_end_or_error
+	end
   in
   let compile_m = externals_factory#add_item "_Compile" ~callback:compile_f in
 
@@ -2255,33 +2260,33 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 			 ))
   in
   let detach_current_view = configuration_factory#add_item 
-		      "De_tach View"
-		      ~callback:
-		      (do_if_not_computing
-			 (fun () -> 
-			    match get_current_view () with  
-			      | {view=v;analyzed_view=Some av} -> 
-			      	  let w = GWindow.window ~show:true 
-				      ~title:(match av#filename with
-						| None -> "*Unnamed*"
-						| Some f -> f) 
-					    () 
-				  in
-				  let sb = GBin.scrolled_window 
-					     ~packing:w#add () 
-				  in
-				  let nv = GText.view 
-					     ~buffer:v#buffer 
-					     ~packing:sb#add 
-					     ()
-				  in
-				  ignore (w#connect#destroy 
-					    ~callback:
-					    (fun () -> av#remove_detached_view w));
-				  av#add_detached_view w
-			      | _ -> ()
-
-			 ))
+			      "De_tach View"
+			      ~callback:
+			      (do_if_not_computing
+				 (fun () -> 
+				    match get_current_view () with  
+				    | {view=v;analyzed_view=Some av} -> 
+			      		let w = GWindow.window ~show:true 
+						  ~title:(match av#filename with
+							  | None -> "*Unamed*"
+							  | Some f -> f) 
+						  () 
+					in
+					let sb = GBin.scrolled_window 
+						   ~packing:w#add () 
+					in
+					let nv = GText.view 
+						   ~buffer:v#buffer 
+						   ~packing:sb#add 
+						   ()
+					in
+					ignore (w#connect#destroy 
+						  ~callback:
+						  (fun () -> av#remove_detached_view w));
+					av#add_detached_view w
+				    | _ -> ()
+
+				 ))
   in
   (* Help Menu *)
 
@@ -2389,37 +2394,37 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 	  !flash_info (t^"\n"^txt);
 	  t = txt)
        with 
-	 | true,true -> 
-	     (!flash_info "T,T";iit#backward_search txt)
-	 | false,true -> !flash_info "F,T";Some (iit,npi)
-	 | _,false ->
-	     (iit#backward_search txt)
+       | true,true -> 
+	   (!flash_info "T,T";iit#backward_search txt)
+       | false,true -> !flash_info "F,T";Some (iit,npi)
+       | _,false ->
+	   (iit#backward_search txt)
 
        with 
-	 | None -> 
-	     if !ready_to_wrap_search then begin
-	       ready_to_wrap_search := false;
-	       !flash_info "Search wrapped";
-	       v#buffer#place_cursor 
-		 (if !search_forward then v#buffer#start_iter else
-		    v#buffer#end_iter);
-	       search_f ()
-	     end else begin
-	       if !search_forward then !flash_info "Search at end"
-	       else !flash_info "Search at start";
-	       ready_to_wrap_search := true
-	     end
-	 | Some (start,stop) -> 
-	     prerr_endline "search: before moving marks";
-	     prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
-	     prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
-
-	     v#buffer#move_mark `SEL_BOUND start;
-	     v#buffer#move_mark `INSERT stop;
-	     prerr_endline "search: after moving marks";
-	     prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
-	     prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
-	     v#scroll_to_mark `SEL_BOUND
+       | None -> 
+	   if !ready_to_wrap_search then begin
+	     ready_to_wrap_search := false;
+	     !flash_info "Search wrapped";
+	     v#buffer#place_cursor 
+	       (if !search_forward then v#buffer#start_iter else
+		  v#buffer#end_iter);
+	     search_f ()
+	   end else begin
+	     if !search_forward then !flash_info "Search at end"
+	     else !flash_info "Search at start";
+	     ready_to_wrap_search := true
+	   end
+       | Some (start,stop) -> 
+	   prerr_endline "search: before moving marks";
+	   prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
+	   prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
+
+	   v#buffer#move_mark `SEL_BOUND start;
+	   v#buffer#move_mark `INSERT stop;
+	   prerr_endline "search: after moving marks";
+	   prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
+	   prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
+	   v#scroll_to_mark `SEL_BOUND
     )
   in
   ignore (search_input#entry#event#connect#key_release 
@@ -2428,16 +2433,16 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 	       if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin
 		 let v = (get_current_view ()).view in
 		 (match !start_of_search with 
-		    | None -> 
-			prerr_endline "search_key_rel: Placing sel_bound";
-			v#buffer#move_mark 
-			  `SEL_BOUND 
-			  (v#buffer#get_iter_at_mark `INSERT)
-		    | Some mk -> let it = v#buffer#get_iter_at_mark 
-					    (`MARK mk) in
-		      prerr_endline "search_key_rel: Placing cursor";
-		      v#buffer#place_cursor it;
-		      start_of_search := None
+		  | None -> 
+		      prerr_endline "search_key_rel: Placing sel_bound";
+		      v#buffer#move_mark 
+			`SEL_BOUND 
+			(v#buffer#get_iter_at_mark `INSERT)
+		  | Some mk -> let it = v#buffer#get_iter_at_mark 
+					  (`MARK mk) in
+		    prerr_endline "search_key_rel: Placing cursor";
+		    v#buffer#place_cursor it;
+		    start_of_search := None
 		 );
 		 search_input#entry#set_text ""; 
 		 v#coerce#misc#grab_focus ();
@@ -2557,7 +2562,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   w#show ();
   message_view := Some tv3;
   proof_view := Some tv2;
-  let view = create_input_tab "*Unnamed Buffer*" in
+  let view = create_input_tab "*Unamed Buffer*" in
   let index = add_input_view {view = view;
 			      analyzed_view = None;
 			     }
@@ -2599,12 +2604,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 	);
   ignore(tv2#event#connect#enter_notify
 	   (fun _ -> 
+	      let w = (out_some (get_active_view ()).analyzed_view) in
 	      !push_info "Computing advanced goal's menus";
 	      prerr_endline "Entering Goal Window. Computing Menus....";
-	      (out_some (get_active_view ()).analyzed_view)#show_goals_full;
+	      w#show_goals_full;
 	      prerr_endline "....Done with Goal menu";
 	      !pop_info();
-	      false));
+	      false;
+	   ));
   List.iter load files;
   if List.length files >=1 then activate_input 1
 ;;
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index ed124461f..94fc0174f 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -14,6 +14,8 @@
   let buff = Buffer.create 513
 }
 
+let phrase_sep = '.'
+
 rule next_phrase = parse
   | "(*" { incr length; incr length; 
 	   skip_comment lexbuf;
@@ -24,7 +26,7 @@ rule next_phrase = parse
 		 Buffer.add_string buff lexeme;
 		 next_phrase lexbuf
 	       }
-  | '.'[' ''\n''\t''\r'] {	
+  | phrase_sep[' ''\n''\t''\r'] {
       length := !length + 2; 
       Buffer.add_string buff (Lexing.lexeme lexbuf);
       Buffer.contents buff}
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 671b12410..e5edce660 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -58,45 +58,61 @@ let process_pending () =
 let print_id id =
   prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id)))
 
+
+let do_convert s = 
+  Utf8_convert.f
+    (if Glib.Utf8.validate s then begin
+       prerr_endline "Input is UTF-8";s
+     end else
+       let from_loc () = 
+	 let _,char_set = Glib.Convert.get_charset () in
+	 prerr_endline 
+	   ("Coqide warning: trying to convert from locale ("^char_set^")");
+	 Glib.Convert.convert_with_fallback ~to_codeset:"UTF-8" ~from_codeset:char_set s
+       in
+       let from_manual () = 
+	 prerr_endline 
+	   ("Coqide warning: trying to convert from "^ !current.encoding_manual);
+	 Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:!current.encoding_manual
+       in
+       if !current.encoding_use_utf8 || !current.encoding_use_locale then begin
+	 try
+	   from_loc ()
+	 with _ -> from_manual ()
+       end else begin
+	 try
+	   from_manual () 
+	 with _ -> from_loc ()
+       end)
+
 let try_convert s = 
   try
-    if Glib.Utf8.validate s then s else
-      (prerr_endline 
-	 "Coqide warning: input is not UTF-8 encoded. Trying to convert from locale.";
-       Glib.Convert.locale_to_utf8 s)
+    do_convert s
   with _ -> 
     "(* Fatal error: wrong encoding in input.
-Please set your locale according to your file encoding.*)"
+Please choose a correct encoding in the preference panel.*)";;
 
-let do_convert s = 
-  if Glib.Utf8.validate s then (prerr_endline "Input is UTF-8";s) else
-    try 
-      (prerr_endline 
-	 "Coqide warning: input is not UTF-8 encoded. Trying to convert from locale.";
-       Glib.Convert.locale_to_utf8 s)
-    with _ -> 
-      (prerr_endline 
-	 "Coqide warning: input is not even LOCALE encoded. Trying to convert from fr_FR.";
-       Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:"ISO-8859-1")
 
 let try_export file_name s = 
-  try 
-    let s = 
-      if (fst (Glib.Convert.get_charset ())) then
-	(prerr_endline "Charset is UTF-8" ;s) 
+  try let s = 
+    try if !current.encoding_use_utf8 then begin
+      (prerr_endline "UTF-8 is enforced" ;s)
+    end else if !current.encoding_use_locale then begin
+      let is_unicode,char_set = Glib.Convert.get_charset () in
+      if is_unicode then 
+	(prerr_endline "Locale is UTF-8" ;s)	
       else
-	(try Glib.Convert.locale_from_utf8 s 
-	 with _ -> 
-(*	   try 
-	     prerr_endline "Warning: exporting to ISO8859-1";
-	     Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:"ISO-8859-1"
-	   with _ -> *)
-	     prerr_endline "Warning: exporting to utf8";s)
-    in
-    let oc = open_out file_name in
-    output_string oc s;
-    close_out oc;
-    true
+	(prerr_endline ("Locale is "^char_set);
+	 Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s)
+    end else 	
+      (prerr_endline ("Manual charset is "^ !current.encoding_manual);
+       Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:!current.encoding_manual s)
+    with e -> (prerr_endline ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s)
+  in
+  let oc = open_out file_name in
+  output_string oc s;
+  close_out oc;
+  true
   with e -> prerr_endline (Printexc.to_string e);false
 
 let browse url =
@@ -171,12 +187,12 @@ let select_file ~title ?(dir = last_dir) ?(filename="") () =
     if Filename.is_relative filename then begin
       if !dir <> "" then
         let filename = Filename.concat !dir filename in 
-        GWindow.file_selection ~modal:true ~title ~filename ()
+        GWindow.file_selection ~fileop_buttons:true ~modal:true ~title ~filename ()
       else
-        GWindow.file_selection ~modal:true ~title ()
+        GWindow.file_selection ~fileop_buttons:true ~modal:true ~title ()
     end else begin
       dir := Filename.dirname filename;
-      GWindow.file_selection ~modal:true ~title ~filename ()
+      GWindow.file_selection ~fileop_buttons:true ~modal:true ~title ~filename ()
     end
   in
   fs#complete ~filter:"";
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 0ee8bec55..9e22a3636 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -67,6 +67,10 @@ type pref =
       mutable auto_save_delay : int;
       mutable auto_save_name : string * string;
 
+      mutable encoding_use_locale : bool;
+      mutable encoding_use_utf8 : bool;
+      mutable encoding_manual : string;
+
       mutable automatic_tactics : (string * string) list;
       mutable cmd_print : string;
 
@@ -85,6 +89,7 @@ type pref =
       mutable show_toolbar : bool;
       mutable window_width : int;
       mutable window_height :int;
+      mutable use_utf8_notation : bool;
 
     }
 
@@ -102,6 +107,10 @@ let (current:pref ref) =
     auto_save = false;
     auto_save_delay = 10000;
     auto_save_name = "#","#";
+    
+    encoding_use_locale = true;
+    encoding_use_utf8 = true;
+    encoding_manual = "ISO_8859-1";
 
     automatic_tactics = ["Progress Trivial.","Trivial.";
 			 "Progress Auto.","Auto.";
@@ -127,6 +136,7 @@ let (current:pref ref) =
     show_toolbar = true;
     window_width = 800;
     window_height = 600; 
+    use_utf8_notation = true;
   }
 
 
@@ -154,6 +164,11 @@ let save_pref () =
     add "auto_save" [string_of_bool p.auto_save] ++
     add "auto_save_delay" [string_of_int p.auto_save_delay] ++
     add "auto_save_name" [fst p.auto_save_name; snd p.auto_save_name] ++
+
+    add "encoding_use_locale" [string_of_bool p.encoding_use_locale] ++
+    add "encoding_use_utf8" [string_of_bool p.encoding_use_utf8] ++
+    add "encoding_manual" [p.encoding_manual] ++
+
     add "automatic_tactics" 
       (List.fold_left (fun l (v1,v2) -> v1::v2::l) [] p.automatic_tactics) ++
     add "cmd_print" [p.cmd_print] ++
@@ -199,6 +214,10 @@ let load_pref () =
     set_bool "auto_save" (fun v -> np.auto_save <- v);
     set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v);
     set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2));
+    set_bool "encoding_use_locale" (fun v -> np.encoding_use_locale <- v);
+    set_bool "encoding_use_utf8" (fun v -> np.encoding_use_utf8 <- v);
+    set_hd "encoding_manual" (fun v -> np.encoding_manual <- v);
+
     set "automatic_tactics"
       (fun v -> 
 	 let rec from_list = function
@@ -231,7 +250,8 @@ let load_pref () =
 
 let configure () = 
   let cmd_coqc = 
-    string ~f:(fun s -> !current.cmd_coqc <- s) "coqc"  !current.cmd_coqc in
+    string
+      ~f:(fun s -> !current.cmd_coqc <- s) "coqc"  !current.cmd_coqc in
   let cmd_make = string ~f:(fun s -> !current.cmd_make <- s)
 		   "make" !current.cmd_make in
   let cmd_coqmakefile = string ~f:(fun s -> !current.cmd_coqmakefile <- s)
@@ -281,6 +301,14 @@ let configure () =
       (string_of_int !current.window_width)
   in  
 
+(*  let use_utf8_notation = 
+    bool 
+      ~f:(fun b -> 
+	    !current.use_utf8_notation <- b;
+	 ) 
+      "Use Unicode Notation: " !current.use_utf8_notation
+  in
+*)  
   let config_appearance = [show_toolbar; window_width; window_height] in
 
   let global_auto_revert = 
@@ -309,6 +337,27 @@ let configure () =
       (string_of_int !current.auto_save_delay)
   in  
 
+  let encodings = 
+    combo 
+      "File charset encoding "
+      ~f:(fun s -> 
+	    match s with
+	    | "UTF-8" -> 
+		!current.encoding_use_utf8 <- true;
+		!current.encoding_use_locale <- false
+	    | "LOCALE" ->
+		!current.encoding_use_utf8 <- false;
+		!current.encoding_use_locale <- true
+	    | _ -> 		
+		!current.encoding_use_utf8 <- false;
+		!current.encoding_use_locale <- false;
+		!current.encoding_manual <- s;
+	 )
+      ~new_allowed: true
+      ["UTF-8";"LOCALE";!current.encoding_manual]
+      (if !current.encoding_use_utf8 then "UTF-8" 
+       else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual)
+  in
   let modifier_for_tactics = 
     modifiers
       ~allow:!current.modifiers_valid
@@ -388,6 +437,7 @@ let configure () =
      Section("Files",
 	     [global_auto_revert;global_auto_revert_delay;
 	     auto_save; auto_save_delay; (* auto_save_name*)
+	     encodings
 	     ]);
      Section("Browser",
 	     [cmd_browse;doc_url;library_url]);
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 055d621d4..abee44d62 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -22,6 +22,10 @@ type pref =
       mutable auto_save_delay : int;
       mutable auto_save_name : string * string;
 
+      mutable encoding_use_locale : bool;
+      mutable encoding_use_utf8 : bool;
+      mutable encoding_manual : string;
+
       mutable automatic_tactics : (string * string) list;
       mutable cmd_print : string;
 
@@ -40,7 +44,7 @@ type pref =
       mutable show_toolbar : bool;
       mutable window_width : int;
       mutable window_height : int;
-
+      mutable use_utf8_notation : bool;
     }
 
 val save_pref : unit -> unit
diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll
new file mode 100644
index 000000000..52772ad68
--- /dev/null
+++ b/ide/utf8_convert.mll
@@ -0,0 +1,51 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+{
+  open Lexing 
+  let b = Buffer.create 127
+
+}
+
+(* Replace all occurences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *)
+
+let digit = ['0'-'9''A'-'Z''a'-'z']
+let short = digit digit digit digit
+let long = short short
+
+rule entry = parse
+  | "\\x{" (short | long ) '}'
+      { let s = lexeme lexbuf in
+	let n = String.length s in
+	let code = 
+	  try Glib.Utf8.from_unichar 
+	    (int_of_string ("0x"^(String.sub s 3 (n - 4)))) 
+	  with _ -> s
+	in
+	let c = if Glib.Utf8.validate code then code else s in
+	Buffer.add_string b c;
+	entry lexbuf
+      }
+  | _ 
+      { let s = lexeme lexbuf in
+	Buffer.add_string b s;
+	entry lexbuf}
+  | eof
+      {
+	let s = Buffer.contents b in Buffer.reset b ; s
+      }
+
+
+{
+  let f s =
+   let lb = from_string s in
+   Buffer.reset b;
+   entry lb
+}
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index d01b83003..835682b69 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -380,7 +380,7 @@ class combo_param_box param =
       None -> ()
     | Some help ->
 	let tooltips = GData.tooltips () in
-	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
+	ignore (hbox#connect#destroy ~callback:tooltips#destroy);
 	tooltips#set_tip wev#coerce ~text: help ~privat: help 
   in
   let _ = wc#entry#set_editable param.combo_editable in