configure pour CoqIde repare

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

5 files changed, 50 insertions, 33 deletions

diff --git a/configure b/configure
index bbd1bb32a..eaaa62fac 100755
--- a/configure
+++ b/configure
@@ -319,12 +319,13 @@ esac
 
 if [ "$coqide_spec" = "no" ] ; then
 if test -x ${CAMLLIB}/lablgtk2; then
-    if grep -q -w convert_with_fallback ${CAMLLIB}/lablgtk2/glib.mli; then
-	COQIDE=byte;
-    fi
-    # native threads
-    if test -f ${CAMLLIB}/threads/threads.cmxa; then
-	COQIDE=opt
+    if grep -q -w convert_with_fallbacks ${CAMLLIB}/lablgtk2/glib.mli; then
+	COQIDE=byte
+	# native threads
+	if test -f ${CAMLLIB}/threads/threads.cmxa; then
+	    COQIDE=opt;
+	fi;
+    else COQIDE=no;
     fi
 else
     COQIDE=no
diff --git a/ide/FAQ b/ide/FAQ
index 2dcbd1dfd..9f533cdfc 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -22,11 +22,12 @@ Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
 ======================================================================
 Copy/Paste of these lines from this file will not work outside of CoqIde.
 You need to load a file containing these lines or to enter the "∀" 
-using an input method (see Q5). As a convenience, you may put these lines in
-a utf8.v file and start coqide with : 
-	coqide -l utf8.v
+using an input method (see Q5). To try it just use "Require utf8" from inside
+CoqIde. 
+To enable these notations automatically start coqide with
+	coqide -l utf8
 In the ide subdir of Coq library, you will find a sample utf8.v with some 
-pretty notations.
+pretty simple notations.
 
 Q5) How to define an input method for non ASCII symbols?
 R5)-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script widow. 
@@ -62,9 +63,11 @@ R7) Two solutions are offered:
     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.
+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 each dot is an hex. digit. 
+ The number between braces is the hexadecimal UNICODE index for the
+  missing character.
     
-    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/blaster_window.ml b/ide/blaster_window.ml
index 414b86c3b..63b6c0675 100644
--- a/ide/blaster_window.ml
+++ b/ide/blaster_window.ml
@@ -11,6 +11,8 @@
 open Gobject.Data
 open Ideutils
 
+exception Stop
+
 class blaster_window (n:int) = 
   let window = GWindow.window 
 		 ~allow_grow:true ~allow_shrink:true 
@@ -68,6 +70,8 @@ object(self)
   val window = window
   val roots = Hashtbl.create 17
   val tbl = Hashtbl.create 17
+  val blaster_lock = Mutex.create () 
+  method lock = blaster_lock 
   method window = window
   method set
     root
@@ -92,23 +96,28 @@ object(self)
 
       
   method blaster () = 
-    view#expand_all ();
-    Hashtbl.iter 
-      (fun k (nt,compute,on_click) ->
-	 match compute () with 
-	 | Coq.Interrupted -> 
-	     prerr_endline "Interrupted"
-	 | Coq.Failed -> 
-	     prerr_endline "Failed";
-	     model#set ~row:nt ~column:status false;
-	     model#set ~row:nt ~column:nb_goals "N/A"
-	     
-	 | Coq.Success n -> 
-	     prerr_endline "Success";
-	     model#set ~row:nt ~column:status true;
-	     model#set ~row:nt ~column:nb_goals (string_of_int n)
-      )
-      tbl
+    if Mutex.try_lock blaster_lock then begin
+      view#expand_all ();
+      try Hashtbl.iter 
+	(fun k (nt,compute,on_click) ->
+	   match compute () with 
+	   | Coq.Interrupted -> 
+	       prerr_endline "Interrupted";
+	       raise Stop
+	   | Coq.Failed -> 
+	       prerr_endline "Failed";
+	       model#set ~row:nt ~column:status false;
+	       model#set ~row:nt ~column:nb_goals "N/A"
+	       
+	   | Coq.Success n -> 
+	       prerr_endline "Success";
+	       model#set ~row:nt ~column:status true;
+	       model#set ~row:nt ~column:nb_goals (string_of_int n)
+	)
+	tbl;
+      Mutex.unlock blaster_lock
+      with Stop -> Mutex.unlock blaster_lock
+    end else prerr_endline "blaster is till computing"
 
   initializer 
     ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));
diff --git a/ide/coqide.ml b/ide/coqide.ml
index cbd5c1d11..719a8fcbe 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1226,7 +1226,7 @@ Please restart and report NOW.";
     else prerr_endline "undo_last_step discarded"
 
       
-  method blaster () = 
+  method blaster () =
     prerr_endline "Blaster called";
     let c = Blaster_window.blaster_window () in
     c#clear ();
diff --git a/ide/utf8.v b/ide/utf8.v
index 801aaa8c2..98c2e9638 100644
--- a/ide/utf8.v
+++ b/ide/utf8.v
@@ -1,5 +1,9 @@
 (* Logic *)
 Notation "∀ x : t , P" := (x:t)P (at level 1, x,t,P at level 10).
+Notation "∀ x y : t , P" := (x:t)(y:t)P (at level 1, x,y,t,P at level 10).
+Notation "∀ x y z : t , P" := (x:t)(y:t)(z:t) P (at level 1, x,y,z,t,P at level 10).
+Notation "∀ x y z u : t , P" := (x:t)(y:t)(z:t)(u:t)P (at level 1, x,y,z,u,t,P at level 10).
+
 Notation "∃ x : t , P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
 Notation "x ∨ y" := (x \/ y) (at level 1, y at level 10).
 Notation "x ∧ y" := (x /\ y) (at level 1, y at level 10).