coqide: warn when using locale or manual charset

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

4 files changed, 29 insertions, 16 deletions

diff --git a/.depend.newcoq b/.depend.newcoq
index 9cdc3b1da4..0aafc1827f 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -63,7 +63,7 @@ newtheories/Init/Specif.vo: newtheories/Init/Specif.v newtheories/Init/Datatypes
 newtheories/Init/LogicSyntax.vo: newtheories/Init/LogicSyntax.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo
 newtheories/Init/SpecifSyntax.vo: newtheories/Init/SpecifSyntax.v newtheories/Init/Notations.vo 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/Wf.vo: newtheories/Init/Wf.v newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Datatypes.vo
 newtheories/Init/Logic_TypeSyntax.vo: newtheories/Init/Logic_TypeSyntax.v newtheories/Init/Notations.vo 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/Logic/Hurkens.vo: newtheories/Logic/Hurkens.v
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 92770be11f..7007d05091 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1,4 +1,4 @@
- (***********************************************************************)
+(***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
 (*   \VV/  *************************************************************)
@@ -31,15 +31,6 @@ let small_size = `SMALL_TOOLBAR
 
 let initial_cwd = Sys.getcwd ()
 
-let status = ref None
-let push_info = ref (function s -> failwith "not ready")
-let pop_info = ref (function s -> failwith "not ready")
-let flash_info = ref  (fun ?delay s -> failwith "not ready")
-
-let set_location = ref  (function s -> failwith "not ready")
-
-let pulse = ref (function () -> failwith "not ready")
-
 let (message_view:GText.view option ref) = ref None
 let (proof_view:GText.view option ref) = ref None
 
@@ -64,7 +55,7 @@ let set_tab_label i n =
   let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget 
   in
   lbl#set_use_markup true;
-  lbl#set_text n
+  lbl#set_text n (* lbl#set_label n *)
 
 let set_tab_image i s = 
   let nb = notebook () in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 8c7a2ec1f4..99c06cf672 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -13,6 +13,18 @@ open Preferences
 
 exception Forbidden
 
+(* status bar and locations *)
+
+let status = ref None
+let push_info = ref (function s -> failwith "not ready")
+let pop_info = ref (function s -> failwith "not ready")
+let flash_info = ref  (fun ?delay s -> failwith "not ready")
+
+let set_location = ref  (function s -> failwith "not ready")
+
+let pulse = ref (function () -> failwith "not ready")
+
+
 let debug = Options.debug
 
 let prerr_endline s =
@@ -66,13 +78,13 @@ let do_convert 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^")");
+	 !flash_info
+	   ("Converting 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);
+	 !flash_info 
+	   ("Converting 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
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 3edc8ef854..6c2124a374 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -52,3 +52,13 @@ val underscore : Glib.unichar
 val bn : Glib.unichar
 val space : Glib.unichar
 val tab : Glib.unichar
+
+
+val status : GMisc.statusbar option ref 
+val push_info : (string -> unit) ref
+val pop_info : (unit -> unit) ref
+val flash_info : (?delay:int -> string -> unit) ref
+
+val set_location : (string -> unit) ref
+
+val pulse : (unit -> unit) ref