diff options
-rw-r--r-- | ide/ideutils.ml | 5 | ||||
-rw-r--r-- | ide/minilib.ml | 2 | ||||
-rw-r--r-- | ide/minilib.mli | 3 | ||||
-rw-r--r-- | ide/project_file.ml4 | 85 | ||||
-rw-r--r-- | tools/coq_makefile.ml | 3 |
5 files changed, 57 insertions, 41 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index c6994a8d9..71ff87f00 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -328,7 +328,4 @@ let browse_keyword f text = try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u) with Not_found -> f ("No documentation found for \""^text^"\".\n") -let absolute_filename f = - if Filename.is_relative f then - Filename.concat (Sys.getcwd ()) f - else f +let absolute_filename f = Minilib.correct_path f (Sys.getcwd ()) diff --git a/ide/minilib.ml b/ide/minilib.ml index 96d257df6..54be52c19 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -122,6 +122,8 @@ let canonical_path_name p = (* We give up to find a canonical name and just simplify it... *) strip_path p +let correct_path f dir = if Filename.is_relative f then Filename.concat dir f else f + (* checks if two file names refer to the same (existing) file by comparing their device and inode. diff --git a/ide/minilib.mli b/ide/minilib.mli index 86f7c8a3f..44e570301 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -30,8 +30,11 @@ val coqtop_path : string ref (avoid exception in win32 without console) *) val safe_prerr_endline : string -> unit +val remove_path_dot : string -> string val strip_path : string -> string val canonical_path_name : string -> string +(** correct_path f dir = dir/f if f is relative *) +val correct_path : string -> string -> string (** checks if two file names refer to the same (existing) file *) val same_file : string -> string -> bool diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 9c7a29045..77d002c28 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -38,54 +38,63 @@ let parse f = close_in c; res -let rec process_cmd_line ((project_file,makefile,install,opt) as opts) l = function +let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function | [] -> opts,List.rev l | ("-h"|"--help") :: _ -> raise Parsing_error | ("-no-opt"|"-byte") :: r -> - process_cmd_line (project_file,makefile,install,false) l r + process_cmd_line orig_dir (project_file,makefile,install,false) l r | ("-full"|"-opt") :: r -> - process_cmd_line (project_file,makefile,install,true) l r + process_cmd_line orig_dir (project_file,makefile,install,true) l r | "-impredicative-set" :: r -> Minilib.safe_prerr_endline "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform."; - process_cmd_line opts (Arg "-impredicative_set" :: l) r + process_cmd_line orig_dir opts (Arg "-impredicative_set" :: l) r | "-no-install" :: r -> if not install then Minilib.safe_prerr_endline "Warning: -no-install sets more than once."; - process_cmd_line (project_file,makefile,false,opt) l r + process_cmd_line orig_dir (project_file,makefile,false,opt) l r | "-custom" :: com :: dependencies :: file :: r -> - process_cmd_line opts (Special (file,dependencies,com) :: l) r + process_cmd_line orig_dir opts (Special (file,dependencies,com) :: l) r | "-I" :: d :: r -> - process_cmd_line opts (Include d :: l) r + process_cmd_line orig_dir opts ((Include (Minilib.correct_path d orig_dir)) :: l) r | "-R" :: p :: lp :: r -> - process_cmd_line opts (RInclude (p,lp) :: l) r + process_cmd_line orig_dir opts (RInclude (Minilib.correct_path p orig_dir,lp) :: l) r | ("-I"|"-custom") :: _ -> raise Parsing_error | "-f" :: file :: r -> + let file = Minilib.correct_path file orig_dir in let () = match project_file with | None -> () | Some _ -> Minilib.safe_prerr_endline "Warning: Several features will not work with multiple project files." - in process_cmd_line (Some file,makefile,install,opt) l ((parse file)@r) + 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 -> - let () = match makefile with - |None -> () - |Some f -> - Minilib.safe_prerr_endline ("Warning: Only one output file in genererated. "^f^" will not.") - in process_cmd_line (project_file,Some file,install,opt) l r + begin try + let _ = String.index file '/' in + raise Parsing_error + with Not_found -> + let () = match makefile with + |None -> () + |Some f -> + Minilib.safe_prerr_endline ("Warning: Only one output file in genererated. "^f^" will not.") + in process_cmd_line orig_dir (project_file,Some file,install,opt) l r + end | v :: "=" :: def :: r -> - process_cmd_line opts (Def (v,def) :: l) r + process_cmd_line orig_dir opts (Def (v,def) :: l) r | "-arg" :: a :: r -> - process_cmd_line opts (Arg a :: l) r + process_cmd_line orig_dir opts (Arg a :: l) r | f :: r -> - process_cmd_line 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 Subdir f) :: l) r + let f = Minilib.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 Subdir f) :: l) r let rec post_canonize f = if Filename.basename f = Filename.current_dir_name @@ -94,32 +103,36 @@ let rec post_canonize f = else f (* Return: ((v,(mli,ml4,ml,mllib),special,subdir),(i_inc,r_inc),(args,defs)) *) -let rec split_arguments = function +let split_arguments = + let rec aux = function | V n :: r -> - let (v,m,o,s),i,d = split_arguments r in ((Minilib.strip_path n::v,m,o,s),i,d) + let (v,m,o,s),i,d = aux r in ((Minilib.remove_path_dot n::v,m,o,s),i,d) | ML n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,Minilib.strip_path n::ml,mllib),o,s),i,d) + let (v,(mli,ml4,ml,mllib),o,s),i,d = aux r in ((v,(mli,ml4,Minilib.remove_path_dot n::ml,mllib),o,s),i,d) | MLI n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(Minilib.strip_path n::mli,ml4,ml,mllib),o,s),i,d) + let (v,(mli,ml4,ml,mllib),o,s),i,d = aux r in ((v,(Minilib.remove_path_dot n::mli,ml4,ml,mllib),o,s),i,d) | ML4 n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,Minilib.strip_path n::ml4,ml,mllib),o,s),i,d) + let (v,(mli,ml4,ml,mllib),o,s),i,d = aux r in ((v,(mli,Minilib.remove_path_dot n::ml4,ml,mllib),o,s),i,d) | MLLIB n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,ml,Minilib.strip_path n::mllib),o,s),i,d) + let (v,(mli,ml4,ml,mllib),o,s),i,d = aux r in ((v,(mli,ml4,ml,Minilib.remove_path_dot n::mllib),o,s),i,d) | Special (n,dep,c) :: r -> - let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d) + let (v,m,o,s),i,d = aux r in ((v,m,(n,dep,c)::o,s),i,d) | Subdir n :: r -> - let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d) + let (v,m,o,s),i,d = aux r in ((v,m,o,n::s),i,d) | Include p :: r -> - let t,(i,r),d = split_arguments r in (t,((post_canonize p,Minilib.canonical_path_name p)::i,r),d) + let t,(i,r),d = aux r in (t,((Minilib.remove_path_dot (post_canonize p), + Minilib.canonical_path_name p)::i,r),d) | RInclude (p,l) :: r -> - let t,(i,r),d = split_arguments r in (t,(i,(post_canonize p,l,Minilib.canonical_path_name p)::r),d) + let t,(i,r),d = aux r in (t,(i,(Minilib.remove_path_dot (post_canonize p),l, + Minilib.canonical_path_name p)::r),d) | Def (v,def) :: r -> - let t,i,(args,defs) = split_arguments r in (t,i,(args,(v,def)::defs)) + let t,i,(args,defs) = aux r in (t,i,(args,(v,def)::defs)) | Arg a :: r -> - let t,i,(args,defs) = split_arguments r in (t,i,(a::args,defs)) + let t,i,(args,defs) = aux r in (t,i,(a::args,defs)) | [] -> ([],([],[],[],[]),[],[]),([],[]),([],[]) + in aux -let read_project_file f = split_arguments (snd (process_cmd_line (Some f, None, false, true) [] (parse f))) +let read_project_file f = split_arguments (snd (process_cmd_line (Filename.dirname f) (Some f, None, false, true) [] (parse f))) let args_from_project file project_files = let contains_file f dir = diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index e26abdb3e..738c1ea2b 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -70,6 +70,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib] [-no-install]: build a makefile with no install target [-f file]: take the contents of file as arguments [-o file]: output should go in file file + Output file outside the current directory is forbidden. [-h]: print this usage summary [--help]: equivalent to [-h]\n"; exit 1 @@ -551,7 +552,7 @@ let do_makefile args = |[] -> var := false |_::_ -> var := true in let (project_file,makefile,is_install,opt),l = - try Project_file.process_cmd_line (None,None,true,true) [] args + try Project_file.process_cmd_line Filename.current_dir_name (None,None,true,true) [] args with Project_file.Parsing_error -> usage () in let (v_f,(mli_f,ml4_f,ml_f,mllib_f),sps,sds as targets), inc, defs = Project_file.split_arguments l in |