Merge PR#406: coq makefile2

3 files changed, 31 insertions, 219 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 663e28d36..a1e78ee3c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -46,7 +46,7 @@ open Session
 
 (** 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 custom_project_file = ref None
 let sup_args = ref []
 
 let logfile = ref None
@@ -81,17 +81,27 @@ let pr_exit_status = function
   | Unix.WEXITED 0 -> " succeeded"
   | _ -> " failed"
 
-let make_coqtop_args = function
-  |None -> "", !sup_args
-  |Some the_file ->
-    let get_args f = Project_file.args_from_project f
-      !custom_project_files project_file_name#get
-    in
-    match read_project#get with
-      |Ignore_args -> "", !sup_args
-      |Append_args ->
-         let fname, args = get_args the_file in fname, args @ !sup_args
-      |Subst_args -> get_args the_file
+let make_coqtop_args fname =
+  let open CoqProject_file in
+  let base_args = match read_project#get with
+    | Ignore_args -> !sup_args
+    | Append_args -> !sup_args
+    | Subst_args -> [] in
+  if read_project#get = Ignore_args then "", base_args
+  else
+    match !custom_project_file, fname with
+    | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args
+    | None, None -> "", base_args
+    | None, Some the_file ->
+       match
+         CoqProject_file.find_project_file
+           ~from:(Filename.dirname the_file)
+           ~projfile_name:project_file_name#get
+       with
+       | None -> "", base_args
+       | Some proj -> 
+           proj, coqtop_args_from_project (read_project_file proj) @ base_args
+;;
 
 (** Setting drag & drop on widgets *)
 
@@ -1345,9 +1355,11 @@ let read_coqide_args argv =
       if coqtop = None then filter_coqtop (Some prog) project_files out args
       else (output_string stderr "Error: multiple -coqtop options"; exit 1)
     |"-f" :: file :: args ->
+      if project_files <> None then
+        (output_string stderr "Error: multiple -f options"; exit 1);
       let d = CUnix.canonical_path_name (Filename.dirname file) in
-      let p = Project_file.read_project_file file in
-      filter_coqtop coqtop ((d,p) :: project_files) out args
+      let p = CoqProject_file.read_project_file file in
+      filter_coqtop coqtop (Some (d,p)) out args
     |"-f" :: [] ->
       output_string stderr "Error: missing project file name"; exit 1
     |"-coqtop" :: [] ->
@@ -1364,11 +1376,11 @@ let read_coqide_args argv =
       (* argument added by MacOS during .app launch *)
       filter_coqtop coqtop project_files out args
     |arg::args -> filter_coqtop coqtop project_files (arg::out) args
-    |[] -> (coqtop,List.rev project_files,List.rev out)
+    |[] -> (coqtop,project_files,List.rev out)
   in
-  let coqtop,project_files,argv = filter_coqtop None [] [] argv in
+  let coqtop,project_files,argv = filter_coqtop None None [] argv in
   Ideutils.custom_coqtop := coqtop;
-  custom_project_files := project_files;
+  custom_project_file := project_files;
   argv
 
 
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 78b4c01e8..57e9fe5ad 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,6 +9,8 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
+Serialize
+Richprinter
 Xml_lexer
 Xml_parser
 Xml_printer
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
deleted file mode 100644
index de0720e03..000000000
--- a/ide/project_file.ml4
+++ /dev/null
@@ -1,202 +0,0 @@
-type target =
-  | ML of string (* ML file : foo.ml -> (ML "foo.ml") *)
-  | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *)
-  | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *)
-  | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *)
-  | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *)
-  | V of string  (* V file : foo.v -> (V "foo") *)
-  | Arg of string
-  | Special of string * string * bool * string
-    (* file, dependencies, is_phony, command *)
-  | Subdir of string
-  | Def of string * string (* X=foo -> Def ("X","foo") *)
-  | MLInclude of string (* -I physicalpath *)
-  | Include of string * string (* -Q physicalpath logicalpath *)
-  | RInclude of string * string (* -R physicalpath logicalpath *)
-
-type install =
-  | NoInstall
-  | TraditionalInstall
-  | UserInstall
-  | UnspecInstall
-
-exception Parsing_error
-let rec parse_string = parser
-  | [< '' ' | '\n' | '\t' >] -> ""
-  | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
-  | [< >] -> ""
-and parse_string2 = parser
-  | [< ''"' >] -> ""
-  | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
-  | [< >] -> raise Parsing_error
-and parse_skip_comment = parser
-  | [< ''\n'; s >] -> s
-  | [< 'c; s >] -> parse_skip_comment s
-  | [< >] -> [< >]
-and parse_args = parser
-  | [< '' ' | '\n' | '\t'; s >] -> parse_args s
-  | [< ''#'; s >] -> parse_args (parse_skip_comment s)
-  | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s
-  | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
-  | [< >] -> []
-
-
-let parse f =
-  let c = open_in f in
-  let res = parse_args (Stream.of_channel c) in
-    close_in c;
-    res
-
-let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function
-  | [] -> opts, l
-  | ("-h"|"--help") :: _ ->
-    raise Parsing_error
-  | ("-no-opt"|"-byte") :: r ->
-    process_cmd_line orig_dir (project_file,makefile,install,false) l r
-  | ("-full"|"-opt") :: r ->
-    process_cmd_line orig_dir (project_file,makefile,install,true) l r
-  | "-impredicative-set" :: r ->
-    Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.");
-    process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r
-  | "-no-install" :: r ->
-    Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead")));
-    process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
-  | "-install" :: d :: r ->
-    if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once.");
-    let install =
-      match d with
-	| "user" -> UserInstall
-	| "none" -> NoInstall
-	| "global" -> TraditionalInstall
-	| _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install.")));
-          install
-    in
-    process_cmd_line orig_dir (project_file,makefile,install,opt) l r
-  | "-custom" :: com :: dependencies :: file :: r ->
-    Feedback.msg_warning (Pp.app
-    (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".")
-    (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.")
-    );
-    process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r
-  | "-extra" :: file :: dependencies :: com :: r ->
-    process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r
-  | "-extra-phony" :: target :: dependencies :: com :: r ->
-    process_cmd_line orig_dir opts (Special (target,dependencies,true,com) :: l) r
-  | "-Q" :: d :: lp :: r ->
-    process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r
-  | "-I" :: d :: r ->
-    process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r
-  | "-R" :: p :: lp :: r ->
-    process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r
-  | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ ->
-    raise Parsing_error
-  | "-f" :: file :: r ->
-    let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
-    let () = match project_file with
-      | None -> ()
-      | Some _ -> Feedback.msg_warning (Pp.str
-	"Several features will not work with multiple project files.")
-    in
-    let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in
-      process_cmd_line orig_dir opts' l' r
-  | ["-f"] ->
-    raise Parsing_error
-  | "-o" :: file :: r ->
-      begin try
-	let _ = String.index file '/' in
-	  raise Parsing_error
-      with Not_found ->
-	let () = match makefile with
-	  |None -> ()
-	  |Some f ->
-	     Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be.")))
-	in process_cmd_line orig_dir (project_file,Some file,install,opt) l r
-      end
-  | v :: "=" :: def :: r ->
-    process_cmd_line orig_dir opts (Def (v,def) :: l) r
-  | "-arg" :: a :: r ->
-    process_cmd_line orig_dir opts (Arg a :: l) r
-  | f :: r ->
-      let f = CUnix.correct_path f orig_dir in
-	process_cmd_line orig_dir opts ((
-          if Filename.check_suffix f ".v" then V f
-	  else if (Filename.check_suffix f ".ml") then ML f
-	  else if (Filename.check_suffix f ".ml4") then ML4 f
-	  else if (Filename.check_suffix f ".mli") then MLI f
-	  else if (Filename.check_suffix f ".mllib") then MLLIB f
-	  else if (Filename.check_suffix f ".mlpack") then MLPACK f
-	  else Subdir f) :: l) r
-
-let process_cmd_line orig_dir opts l args =
-  let (opts, l) = process_cmd_line orig_dir opts l args in
-  opts, List.rev l
-
-let rec post_canonize f =
-  if Filename.basename f = Filename.current_dir_name
-  then let dir = Filename.dirname f in
-    if dir = Filename.current_dir_name then f else post_canonize dir
-  else f
-
-(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *)
-let split_arguments args =
-  List.fold_right
-    (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t),
-            (ml_inc,q_inc,r_inc as i),(args,defs as d)) ->
-     match a with
-     | V n ->
-        ((CUnix.remove_path_dot n::v,m,o,s),i,d)
-     | ML n ->
-        ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d)
-     | MLI n ->
-        ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d)
-     | ML4 n ->
-        ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d)
-     | MLLIB n ->
-        ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d)
-     | MLPACK n ->
-        ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d)
-     | Special (n,dep,is_phony,c) ->
-        ((v,m,(n,dep,is_phony,c)::o,s),i,d)
-     | Subdir n ->
-        ((v,m,o,n::s),i,d)
-     | MLInclude p ->
-        let ml_new = (CUnix.remove_path_dot (post_canonize p),
-                      CUnix.canonical_path_name p) in
-        (t,(ml_new::ml_inc,q_inc,r_inc),d)
-     | Include (p,l) ->
-        let q_new = (CUnix.remove_path_dot (post_canonize p),l,
-		     CUnix.canonical_path_name p) in
-        (t,(ml_inc,q_new::q_inc,r_inc),d)
-     | RInclude (p,l) ->
-        let r_new = (CUnix.remove_path_dot (post_canonize p),l,
-		     CUnix.canonical_path_name p) in
-        (t,(ml_inc,q_inc,r_new::r_inc),d)
-     | Def (v,def) ->
-        (t,i,(args,(v,def)::defs))
-     | Arg a ->
-        (t,i,(a::args,defs)))
-    args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[]))
-
-let read_project_file f =
-  split_arguments
-    (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f)))
-
-let args_from_project file project_files default_name =
-  let build_cmd_line ml_inc i_inc r_inc args =
-    List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc
-      (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: 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 [])))
-  in try
-      let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in
-	fname, build_cmd_line ml_inc i_inc r_inc args
-    with Failure _ ->
-      let rec find_project_file dir = try
-	let fname = Filename.concat dir default_name in
-	let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) =
-          read_project_file fname in
-	fname, build_cmd_line ml_inc i_inc r_inc args
-      with Sys_error s ->
-	let newdir = Filename.dirname dir in
-	  if dir = newdir then "",[] else find_project_file newdir
-      in find_project_file (Filename.dirname file)