coqide: thread bug fix

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

4 files changed, 27 insertions, 16 deletions

diff --git a/.depend.newcoq b/.depend.newcoq
index d4bd8641e..0f0e7b9a5 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -77,7 +77,7 @@ newtheories/Logic/ClassicalFacts.vo: newtheories/Logic/ClassicalFacts.v
 newtheories/Logic/Berardi.vo: newtheories/Logic/Berardi.v
 newtheories/Logic/Eqdep_dec.vo: newtheories/Logic/Eqdep_dec.v
 newtheories/Logic/Decidable.vo: newtheories/Logic/Decidable.v
-newtheories/Logic/JMeq.vo: newtheories/Logic/JMeq.v
+newtheories/Logic/JMeq.vo: newtheories/Logic/JMeq.v newtheories/Logic/Eqdep.vo
 newtheories/Arith/Arith.vo: newtheories/Arith/Arith.v newtheories/Arith/Le.vo newtheories/Arith/Lt.vo newtheories/Arith/Plus.vo newtheories/Arith/Gt.vo newtheories/Arith/Minus.vo newtheories/Arith/Mult.vo newtheories/Arith/Between.vo newtheories/Arith/Peano_dec.vo newtheories/Arith/Compare_dec.vo
 newtheories/Arith/Gt.vo: newtheories/Arith/Gt.v newtheories/Arith/Le.vo newtheories/Arith/Lt.vo newtheories/Arith/Plus.vo
 newtheories/Arith/Between.vo: newtheories/Arith/Between.v newtheories/Arith/Le.vo newtheories/Arith/Lt.vo
@@ -240,7 +240,7 @@ newtheories/Setoids/Setoid.vo: newtheories/Setoids/Setoid.v
 newtheories/Sorting/Heap.vo: newtheories/Sorting/Heap.v newtheories/Lists/PolyList.vo newtheories/Sets/Multiset.vo newtheories/Sorting/Permutation.vo newtheories/Relations/Relations.vo newtheories/Sorting/Sorting.vo
 newtheories/Sorting/Permutation.vo: newtheories/Sorting/Permutation.v newtheories/Relations/Relations.vo newtheories/Lists/PolyList.vo newtheories/Sets/Multiset.vo
 newtheories/Sorting/Sorting.vo: newtheories/Sorting/Sorting.v newtheories/Lists/PolyList.vo newtheories/Sets/Multiset.vo newtheories/Sorting/Permutation.vo newtheories/Relations/Relations.vo
-newcontrib/omega/Omega.vo: newcontrib/omega/Omega.v newtheories/ZArith/fast_integer.vo newtheories/ZArith/zarith_aux.vo newtheories/ZArith/auxiliary.vo newtheories/ZArith/Zsyntax.vo newtheories/ZArith/ZArith_dec.vo newtheories/ZArith/Zmisc.vo newtheories/ZArith/Wf_Z.vo newtheories/ZArith/Zhints.vo newtheories/Arith/Minus.vo
+newcontrib/omega/Omega.vo: newcontrib/omega/Omega.v newtheories/ZArith/fast_integer.vo newtheories/ZArith/zarith_aux.vo newtheories/ZArith/auxiliary.vo newtheories/ZArith/Zsyntax.vo newtheories/ZArith/ZArith_dec.vo newtheories/ZArith/Zmisc.vo newtheories/ZArith/Wf_Z.vo newtheories/ZArith/Zhints.vo
 newcontrib/romega/ReflOmegaCore.vo: newcontrib/romega/ReflOmegaCore.v newtheories/Arith/Arith.vo newtheories/Lists/PolyList.vo newtheories/Bool/Bool.vo newtheories/ZArith/ZArith_base.vo
 newcontrib/romega/ROmega.vo: newcontrib/romega/ROmega.v newcontrib/omega/Omega.vo newcontrib/romega/ReflOmegaCore.vo
 newcontrib/ring/ArithRing.vo: newcontrib/ring/ArithRing.v newcontrib/ring/Ring.vo newtheories/Arith/Arith.vo newtheories/Logic/Eqdep_dec.vo
diff --git a/INSTALL.ide b/INSTALL.ide
index ff5088dc4..f1144c694 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -15,7 +15,7 @@ REQUIREMENT:
 	  You may still compile CoqIde with older 2.0.x versions and 
           use all features.
 	  Run 
-		"pkg-config --modversion gtk+-2.0"
+		"pkg-config --modversion gtk+-2.0 gthread-2.0"
 	  to check your version.
 	 All recent distributions have precompiled packages.
 	 Do not forget to install the developement headers packages.
@@ -26,27 +26,32 @@ REQUIREMENT:
 INSTALLATION
  1) You need to install the OCaml stub library lablgtk2. See 
        		http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
-	  The first official beta snapshot is needed.
+	  No current The latest CVS version is needed.
 	  Use this one :
-http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk2-beta.tar.gz
+	http://www.lri.fr/~monate/download/lablgtk2-coqide.tgz
     If you are in a hurry just run :
     
     cd /tmp && \
-    wget http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk2-beta.tar.gz && \
-    tar zxvf lablgtk2-beta.tar.gz && \
-    cd lablgtk2-beta && \
+    wget http://www.lri.fr/~monate/download/lablgtk2-coqide.tgz && \
+    tar zxvf lablgtk2-coqide.tgz && \
+    cd lablgtk2 && \
     make configure && \
     make all opt && \
     make install
 
    You must have write access to the OCaml standard library path.
-   If this fails read lablgtk2-beta/README.
+   If this fails read lablgtk2/README.
 
 2) Go into your Coq source directory and then : 
 
    make ide
+   
+   In case you are upgrading from an old version you may need to run
+	make clean-ide
 
 3) You may now run bin/coqide.opt or bin/coqide.byte.
+   If your coq install is not local, use 
+	make install-ide
 
 NOTES
 Font configuration is not saved.
diff --git a/Makefile b/Makefile
index 5124b487d..c4f712fd2 100644
--- a/Makefile
+++ b/Makefile
@@ -384,6 +384,8 @@ FULLIDELIB=$(FULLCOQLIB)/ide
 IDEFILES=ide/coq.png ide/.coqiderc
 
 ide: $(COQIDEBYTE) $(COQIDE) states
+clean-ide: 
+	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT)
 
 $(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQIDECMX)
 	$(COQMKTOP) -ide -opt $(OPTFLAGS) -o $@
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 46299c53b..dfcedc826 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -9,13 +9,13 @@ let cb_ = ref None
 let cb () = out_some !cb_
 let last_cb_content = ref ""
 
-let yes_icon = "gtk-yes"
-let no_icon = "gtk-no"
-let save_icon = "gtk-save"
-let saveas_icon = "gtk-save-as"
-let warning_icon = "gtk-dialog-warning"
-let dialog_size = 6
-let small_size = 1
+let yes_icon = `YES
+let no_icon = `NO
+let save_icon = `SAVE
+let saveas_icon = `SAVE_AS
+let warning_icon = `DIALOG_WARNING
+let dialog_size = `DIALOG
+let small_size = `SMALL_TOOLBAR
 
 let window_width = 800
 let window_height = 600
@@ -227,6 +227,7 @@ let full_do_if_not_computing f x =
 if Mutex.try_lock coq_computing then 
   ignore (Thread.create 
 	    (fun () ->
+	       Glib.Thread.enter ();
 	       prerr_endline "Launching thread";
 	       begin
 		   prerr_endline "Getting lock";
@@ -234,9 +235,11 @@ if Mutex.try_lock coq_computing then
 		   f x;
 		   prerr_endline "Releasing lock";
 		   Mutex.unlock coq_computing;
+		   Glib.Thread.leave ();
 		 with e -> 
 		   prerr_endline "Releasing lock (on error)";
 		   Mutex.unlock coq_computing;
+		   Glib.Thread.leave ();
 		   raise e
 	       end)
 	    ())
@@ -2156,6 +2159,7 @@ let start () =
   (try 
      GtkMain.Rc.add_default_file (Filename.concat (Sys.getenv "HOME") ".coqiderc");
   with Not_found -> ());
+  Glib.Thread.init ();
   ignore (GtkMain.Main.init ());
   GtkData.AccelGroup.set_default_mod_mask 
     (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);