*** empty log message ***

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

3 files changed, 17 insertions, 7 deletions

diff --git a/INSTALL.ide b/INSTALL.ide
index f1144c6944..7e08a23724 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -9,6 +9,7 @@ DISCLAIMER: CoqIde is ongoing work. Eventhough it should never let you
  	    Do not hesitate to send suggestions/bug reports.
 
 REQUIREMENT:
+	- OCaml >= 3.06 with native thread support.
 	- make world must succeed.
 	- The graphical toolkit Gtk 2.x. See http://www.gtk.org.
 	  The official supported version is at least 2.2.x.
@@ -24,9 +25,18 @@ REQUIREMENT:
 	 should be enough.
 
 INSTALLATION
+ 0) For optimal performance, OCaml must support native threads (aka
+	pthreads). 
+	If this not the case, this means that Coq computations will be
+	slow and "make ide" will fail. Use "make bin/coqide.byte"
+	instead. To fix this problem, just recompile OCaml from source
+	and configure with : "./configure --with-pthreads". 
+	In case you install over an existing copy of OCaml, you
+	should better empty the OCaml installation directory.
+
  1) You need to install the OCaml stub library lablgtk2. See 
        		http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
-	  No current The latest CVS version is needed.
+	  The latest CVS version is needed.
 	  Use this one :
 	http://www.lri.fr/~monate/download/lablgtk2-coqide.tgz
     If you are in a hurry just run :
diff --git a/ide/coqide.ml b/ide/coqide.ml
index c38188987e..b8a2d0e940 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1097,7 +1097,7 @@ Please restart and report NOW.";
 
   method undo_last_step =
     if Mutex.try_lock coq_may_stop then  
-      (!push_info "Undoing...";
+      (!push_info "Undoing last step...";
        (try
 	  let last_command = top () in
 	  let start = input_buffer#get_iter_at_mark last_command.start in
@@ -1147,7 +1147,7 @@ Please restart and report NOW.";
 		self#backtrack_to_no_lock start
 	  end;
 	with
-	  | Size 0 -> !flash_info "Nothing to Undo"
+	  | Size 0 -> (* !flash_info "Nothing to Undo"*)()
        );
        !pop_info ();
        Mutex.unlock coq_may_stop)
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index e7c5b1073c..d5d1490fe0 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -60,7 +60,7 @@ let try_convert s =
 Please set your locale according to your file encoding.*)"
 
 let do_convert s = 
-  if Glib.Utf8.validate s then s else
+  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.";
@@ -74,14 +74,14 @@ let try_export file_name s =
   try 
     let s = 
       if (fst (Glib.Convert.get_charset ())) then
-	s 
+	(prerr_endline "Charset is UTF-8" ;s) 
       else
 	(try Glib.Convert.locale_from_utf8 s 
 	 with _ -> 
-	   try 
+(*	   try 
 	     prerr_endline "Warning: exporting to ISO8859-1";
 	     Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:"ISO-8859-1"
-	   with _ -> 
+	   with _ -> *)
 	     prerr_endline "Warning: exporting to utf8";s)
     in
     let oc = open_out file_name in