Add option -f to coqide

to specify where to look the project file

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

6 files changed, 41 insertions, 15 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 01a0b3221..85b331c43 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -577,6 +577,7 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
 
 (** The arguments that will be passed to coqtop. No quoting here, since
     no /bin/sh when using create_process instead of open_process. *)
+let custom_project_files = ref []
 let sup_args = ref []
 
 class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct _fn =
@@ -1474,7 +1475,14 @@ let create_session file =
 				      |Some f -> (Glib.Convert.filename_to_utf8 (Filename.basename f))
 				   ) () in
   let stack = Stack.create () in
-  let ct = ref (Coq.spawn_coqtop !sup_args) in
+  let coqtop_args = match file with
+    |None -> !sup_args
+    |Some the_file -> match !current.read_project with
+	|Ignore_args -> !sup_args
+	|Append_args -> (Project_file.args_from_project the_file !custom_project_files)@(!sup_args)
+	|Subst_args -> Project_file.args_from_project the_file !custom_project_files
+  in
+  let ct = ref (Coq.spawn_coqtop coqtop_args) in
   let command = new Command_windows.command_window !ct current in
   let legacy_av = new analyzed_view script proof message stack ct file in
   let () = legacy_av#update_stats in
@@ -2899,19 +2907,24 @@ let default_coqtop_path () =
     prog
   with _ -> "coqtop"
 
-let set_coqtop_path argv =
-  let coqtop = ref "" in
-  let rec filter_coqtop = function
+let read_coqide_args argv =
+  let rec filter_coqtop coqtop project_files out = function
     | "-coqtop" :: prog :: args ->
-      if !coqtop = "" then
-	(coqtop:=prog; filter_coqtop args)
+      if coqtop = "" then filter_coqtop prog project_files out args
       else
 	(output_string stderr "Error: multiple -coqtop options"; exit 1)
-    | arg::args -> arg::filter_coqtop args
-    | [] -> (if !coqtop = "" then coqtop := default_coqtop_path (); [])
+    | "-f" :: file :: args ->
+	filter_coqtop coqtop
+	  ((Minilib.canonical_path_name (Filename.dirname file),
+	    Project_file.read_project_file file) :: project_files) out args
+    | "-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1
+    | arg::args -> filter_coqtop coqtop project_files (arg::out) args
+    | [] -> ((if coqtop = "" then default_coqtop_path () else coqtop),
+	     List.rev project_files,List.rev out)
   in
-  let argv = filter_coqtop argv in
-  Minilib.coqtop_path := !coqtop;
+  let coqtop,project_files,argv = filter_coqtop "" [] [] argv in
+    Minilib.coqtop_path := coqtop;
+    custom_project_files := project_files;
   argv
 
 let process_argv argv =
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 19021ee2c..38b0fab0d 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -12,9 +12,9 @@
     no /bin/sh when using create_process instead of open_process. *)
 val sup_args : string list ref
 
-(** Filter the argv from the option -coqtop, and set
+(** Filter the argv from coqide specific options, and set
     Minilib.coqtop_path accordingly *)
-val set_coqtop_path : string list -> string list
+val read_coqide_args : string list -> string list
 
 (** Ask coqtop the remaining options it doesn't recognize *)
 val process_argv : string list -> string list
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 28301ff1d..a9aed9599 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -66,7 +66,7 @@ END
 
 let () =
   let argl = Array.to_list Sys.argv in
-  let argl = Coqide.set_coqtop_path argl in
+  let argl = Coqide.read_coqide_args argl in
   let files = Coqide.process_argv argl in
   let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
   Coq.check_connection args;
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 8f3a6c353..9bbf9b0d9 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -13,6 +13,7 @@ Typed_notebook
 Config_lexer
 Utf8_convert
 Preferences
+Project_file
 Ideutils
 Ideproof
 Coq_lex
@@ -22,5 +23,4 @@ Coq
 Coq_commands
 Command_windows
 Coqide_ui
-Project_file
 Coqide
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 85e195dae..a8527ac01 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -341,4 +341,3 @@ let absolute_filename f =
   if Filename.is_relative f then
     Filename.concat (Sys.getcwd ()) f
   else f
-
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index ef39b904c..95a0831d8 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -119,3 +119,17 @@ let rec split_arguments = function
   | Arg a :: r ->
       let t,i,(args,defs) = split_arguments r in (t,i,(a::args,defs))
   | [] -> ([],([],[],[],[]),[],[]),([],[]),([],[])
+
+let read_project_file f = split_arguments (snd (process_cmd_line (Some f, None, false, true) [] (parse f)))
+
+let args_from_project file project_files =
+  let contains_file f dir =
+    let is_f = Minilib.same_file f in
+      List.exists (fun x -> is_f (if Filename.is_relative x then Filename.concat dir x else x))
+  in try
+      let (_,(_,(i_inc,r_inc),(args,_))) = List.find (fun (dir,((v_files,_,_,_),_,_)) ->
+							contains_file file dir v_files) project_files in
+	List.fold_right (fun (_,i) o -> "-I" :: i :: o) i_inc
+	  (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc
+	     (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args []))
+    with Not_found -> []