Changement de l'option -where: on vérifie si la variable d'environnement COQLIB est définie

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

6 files changed, 44 insertions, 45 deletions

diff --git a/configure b/configure
index be6c2d0bca..9430dbca7d 100755
--- a/configure
+++ b/configure
@@ -6,8 +6,8 @@
 # 
 ##################################
 
-VERSION=8.1-alpha
-DATE="Mar 2006"
+VERSION=8.1beta
+DATE="Jun 2006"
 
 # a local which command for sh
 which () {
diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml
index 895c57ccd2..400eb1025d 100644
--- a/ide/blaster_window.ml
+++ b/ide/blaster_window.ml
@@ -77,22 +77,17 @@ object(self)
   val blaster_killed = Condition.create () 
   method blaster_killed = blaster_killed
   method window = window
-  method set
-    root
-    name
-    (compute:unit -> Coq.tried_tactic) 
-    (on_click:unit -> unit) 
-    = 
+  method set root name (compute:unit -> Coq.tried_tactic) (on_click:unit -> unit) = 
     let root_iter = 
       try Hashtbl.find roots root 
       with Not_found -> 
 	let nr = new_arg root in
-	Hashtbl.add roots root nr;
-	nr
+	  Hashtbl.add roots root nr;
+	  nr
     in
     let nt = new_tac root_iter name in
     let old_val = try MyMap.find root tbl with Not_found -> MyMap.empty in
-    tbl <- MyMap.add root (MyMap.add name (nt,compute,on_click) old_val) tbl
+      tbl <- MyMap.add root (MyMap.add name (nt,compute,on_click) old_val) tbl
 
   method clear () = 
     model#clear ();      
@@ -107,20 +102,20 @@ object(self)
 	   MyMap.iter 
 	     (fun name (nt,compute,on_click) ->  
 		match compute () with 
-		| Coq.Interrupted -> 
-		    prerr_endline "Interrupted";
-		    raise Stop
-		| Coq.Failed -> 
-		    prerr_endline "Failed";
-		    ignore (model#remove nt)
-		      (*	       model#set ~row:nt ~column:status false;
+		  | Coq.Interrupted -> 
+		      prerr_endline "Interrupted";
+		      raise Stop
+		  | Coq.Failed -> 
+		      prerr_endline "Failed";
+		      ignore (model#remove nt)
+			(*	       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);
-		    if n= -1 then raise Done 
+			*)
+		  | Coq.Success n -> 
+		      prerr_endline "Success";
+		      model#set ~row:nt ~column:status true;
+		      model#set ~row:nt ~column:nb_goals (string_of_int n);
+		      if n= -1 then raise Done 
 	     )
 	     l
 	 with Done -> ())
diff --git a/ide/coq.ml b/ide/coq.ml
index 70d0cf5e4a..62175aee81 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -72,21 +72,21 @@ let is_in_coq_lib dir =
   prerr_endline ("Is it a coq theory ? : "^dir);
   try
     let stat = Unix.stat dir in
-    List.exists 
-      (fun s -> 
-	 try
-	   let fdir = Filename.concat 
-			Coq_config.coqlib 
-			(Filename.concat "theories" s) 
-	   in
-	   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) && 
-           (prerr_endline " YES";true)
-	 with _ -> prerr_endline " No(because of a local exn)";false
-      )
-      Coq_config.theories_dirs
+      List.exists 
+	(fun s -> 
+	   try
+	     let fdir = Filename.concat 
+	       Coq_config.coqlib 
+	       (Filename.concat "theories" s) 
+	     in
+	       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) && 
+		   (prerr_endline " YES";true)
+	   with _ -> prerr_endline " No(because of a local exn)";false
+	)
+	Coq_config.theories_dirs
   with _ -> prerr_endline " No(because of a global exn)";false
 
 let is_in_loadpath dir = Library.is_in_load_paths (System.physical_path_of_string dir)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 832048c08a..1fb1a61165 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -252,7 +252,8 @@ let do_if_not_computing text f x =
     then 
       begin
 	let w = Blaster_window.blaster_window () in
-	  if not (Mutex.try_lock w#lock) then begin 
+	  if not (Mutex.try_lock w#lock) then 
+	    begin 
 	      break ();
 	      let lck = Mutex.create () in
 		Mutex.lock lck;
@@ -260,7 +261,9 @@ let do_if_not_computing text f x =
 		Condition.wait w#blaster_killed lck;
 		prerr_endline "Waiting on blaster ok";
 		Mutex.unlock lck
-	    end else Mutex.unlock w#lock;
+	    end 
+	  else 
+	    Mutex.unlock w#lock;
 	  let idle = 
 	    Glib.Timeout.add ~ms:300
 	      ~callback:(fun () -> async !pulse ();true) in
@@ -280,7 +283,8 @@ let do_if_not_computing text f x =
       end 
     else 
       prerr_endline 
-	"Discarded order (computations are ongoing)" in
+	"Discarded order (computations are ongoing)" 
+  in
     prerr_endline ("Launching thread " ^ text);
     ignore (Thread.create threaded_task ())
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index e0018528d4..27c7734108 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -314,8 +314,8 @@ let same_file f1 f2 =
     let s1 = Unix.stat f1
     and s2 = Unix.stat f2 
     in
-    (s1.Unix.st_dev = s2.Unix.st_dev) &&
-    (s1.Unix.st_ino = s2.Unix.st_ino) 
+      (s1.Unix.st_dev = s2.Unix.st_dev) &&
+	(s1.Unix.st_ino = s2.Unix.st_ino) 
   with
       Unix.Unix_error _ -> false
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e74cad5623..0aaf9675bf 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -244,7 +244,7 @@ let parse_args is_ide =
     | "-vm" :: rem -> use_vm := true; parse rem
     | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem
 	  
-    | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
+    | "-where" :: _ -> print_endline getenv_else "COQLIB" Coq_config.coqlib; exit 0
 
     | ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem