diff options
| -rw-r--r-- | ide/coqide.ml | 12 | ||||
| -rw-r--r-- | ide/project_file.ml4 | 22 |
2 files changed, 15 insertions, 19 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 861689800..87efd17d2 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -84,14 +84,15 @@ let pr_exit_status = function | _ -> " failed" let make_coqtop_args = function - |None -> !sup_args + |None -> "", !sup_args |Some the_file -> let get_args f = Project_file.args_from_project f !custom_project_files prefs.project_file_name in match prefs.read_project with - |Ignore_args -> !sup_args - |Append_args -> get_args the_file @ !sup_args + |Ignore_args -> "", !sup_args + |Append_args -> + let fname, args = get_args the_file in fname, args @ !sup_args |Subst_args -> get_args the_file (** Setting drag & drop on widgets *) @@ -120,7 +121,10 @@ let set_drag (w : GObj.drag_ops) = (** Session management *) let create_session f = - let ans = Session.create f (make_coqtop_args f) in + let project_file, args = make_coqtop_args f in + if project_file <> "" then + flash_info (Printf.sprintf "Reading options from %s" project_file); + let ans = Session.create f args in let _ = set_drag ans.script#drag in ans diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 41dc1befa..f7279f9cf 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -182,29 +182,21 @@ let read_project_file f = (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f))) let args_from_project file project_files default_name = - let is_f = CUnix.same_file file in - let contains_file dir = - List.exists (fun x -> is_f (CUnix.correct_path x dir)) - in 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 (_,(_,(ml_inc,i_inc,r_inc),(args,_))) = - List.find (fun (dir,((v_files,_,_,_),_,_)) -> - contains_file dir v_files) project_files in - build_cmd_line ml_inc i_inc r_inc args - with Not_found -> + 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 (Filename.concat dir default_name) in - if contains_file dir v_files - then build_cmd_line ml_inc i_inc r_inc args - else let newdir = Filename.dirname dir in - if dir = newdir then [] else find_project_file newdir + 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 + if dir = newdir then "",[] else find_project_file newdir in find_project_file (Filename.dirname file) |