diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-01 13:48:47 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-06 22:31:20 +0100 |
| commit | ed98716036e9d47efb2ba66cf0336fc45e03f793 (patch) | |
| tree | 10866ccd6be614ad70b92d4609139db534af8bf7 /lib | |
| parent | 7e0eeba3e91cd5da029aaa6b9c86f7a13f505b88 (diff) | |
Closes #6830: coqdep reads options and files from _CoqProject.
Note that we don't look inside -arg for eg -coqlib.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coqProject_file.ml4 | 8 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 6 |
2 files changed, 14 insertions, 0 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 238e26c42..aeae99b21 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -220,9 +220,17 @@ let rec find_project_file ~from ~projfile_name = else find_project_file ~from:newdir ~projfile_name ;; +let all_files { v_files; ml_files; mli_files; ml4_files; + mllib_files; mlpack_files } = + v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files + let map_sourced_list f l = List.map (fun x -> f x.thing) l ;; +let map_cmdline f l = CList.map_filter (function + | {thing=x; source=CmdLine} -> Some (f x) + | {source=ProjectFile} -> None) l + let coqtop_args_from_project { ml_includes; r_includes; q_includes; extra_args } = diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 68bc5dfe4..97367b600 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -53,8 +53,14 @@ val read_project_file : string -> project val coqtop_args_from_project : project -> string list val find_project_file : from:string -> projfile_name:string -> string option +val all_files : project -> string sourced list + val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list +(** Only uses the elements with source=CmdLine *) +val map_cmdline : ('a -> 'b) -> 'a sourced list -> 'b list + +(** Only uses the elements with source=CmdLine *) val filter_cmdline : 'a sourced list -> 'a list val forget_source : 'a sourced -> 'a |