coqide: maj commandes

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

4 files changed, 39 insertions, 14 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index f442eac2b8..d202f42fb0 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -75,31 +75,32 @@ object(self)
     let result = GText.view ~packing:r_bin#add () in
     result#misc#set_can_focus false;
     result#set_editable false;
+    let callback () =
+      let phrase = combo#entry#text ^ " " ^ entry#text ^" . " in
+      try
+	ignore(Coq.interp phrase);
+	result#buffer#set_text (Ideutils.read_stdout ())
+      with e ->
+	let (s,loc) = Coq.process_exn e in
+	assert (Glib.Utf8.validate s);
+	result#buffer#set_text s
+    in
+
     begin match command,term with 
       | None,None -> ()
       | Some c, None -> 
-	  combo#entry#set_text c
+	  combo#entry#set_text c;
 	  
       | Some c, Some t -> 
 	  combo#entry#set_text c;
 	  entry#set_text t
-
+	 
       | None , Some t -> 
 	  entry#set_text t
     end;
+    callback ();
     entry#misc#grab_focus ();
     entry#misc#grab_default ();
-
-    let callback () =
-      let phrase = combo#entry#text ^ " " ^ entry#text ^" . " in
-      try 
-	ignore(Coq.interp phrase);
-	result#buffer#set_text (Ideutils.read_stdout ())
-      with e ->
-	let (s,loc) = Coq.process_exn e in
-	assert (Glib.Utf8.validate s);
-	result#buffer#set_text s
-    in
     ignore (entry#connect#activate ~callback);
     ignore (combo#entry#connect#activate ~callback);
     self#window#present ()
diff --git a/ide/coq.ml b/ide/coq.ml
index 04f45c24d9..32d21ad1c6 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -32,6 +32,26 @@ let version () =
   Printf.sprintf "The Coq Proof Assistant, version %s (%s)\nCompiled on %s\n"
     Coq_config.version Coq_config.date Coq_config.compile_date
 
+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 dir in 
+	   fstat.Unix.st_dev = stat.Unix.st_dev &&
+	   fstat.Unix.st_ino = stat.Unix.st_ino 
+	 with _ -> false
+      )
+      Coq_config.theories_dirs
+  with _ -> false
+
 let interp s = 
   prerr_endline s;
   flush stderr;
diff --git a/ide/coq.mli b/ide/coq.mli
index bcdd10375a..faf35e6163 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -36,3 +36,6 @@ val reset_to : identifier -> unit
 
 val hyp_menu : hyp -> (string * string) list
 val concl_menu : concl -> (string * string) list
+
+val is_in_coq_lib : string -> bool
+
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 368ef6d9fc..e8b28ec445 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -975,7 +975,8 @@ object(self)
 		 | Some f -> Filename.dirname f
 	      )
     in 
-    ignore (Coq.interp (Printf.sprintf "Add LoadPath \"%s\". " dir));
+    if not (is_in_coq_lib dir) then 
+      ignore (Coq.interp (Printf.sprintf "Add LoadPath \"%s\". " dir));
     Sys.chdir dir