diff options
| author | Emilio Jesus Gallego Arias | 2018-11-06 11:33:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 06:37:05 +0100 |
| commit | 4e9bc09df64cd15e85c19ecabbc9580c00771176 (patch) | |
| tree | d5a9c68561a5d7573641053580b95bc3c7c9be43 /lib/coqProject_file.ml | |
| parent | f8a76b3d383abf468fb21df509f5da8f8aafa913 (diff) | |
[CoqProject] Abstract warning function for CoqProject readers.
`CoqProject_file` uses the feedback system, however this is not very
convenient in some scenarios such as `coqdep` that has to be run very
early in the build process [and thus in "boot" mode].
We thus make the warning function a paramater.
Should fix #8913.
Diffstat (limited to 'lib/coqProject_file.ml')
| -rw-r--r-- | lib/coqProject_file.ml | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index 7395654022..868042303d 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -12,10 +12,6 @@ ideally we would like to make this independent so it can be bootstrapped. *) -(* Note the problem with the error invokation below calling exit... *) -(* let error msg = Feedback.msg_error msg *) -let warning msg = Feedback.msg_warning Pp.(str msg) - type arg_source = CmdLine | ProjectFile type 'a sourced = { thing : 'a; source : arg_source } @@ -147,7 +143,7 @@ let exists_dir dir = try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false -let process_cmd_line orig_dir proj args = +let process_cmd_line ~warning_fn orig_dir proj args = let parsing_project_file = ref (proj.project_file <> None) in let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in let orig_dir = (* avoids turning foo.v in ./foo.v *) @@ -170,7 +166,7 @@ let process_cmd_line orig_dir proj args = | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r | "-install" :: d :: r -> if proj.install_kind <> None then - (warning "-install set more than once.@\n%!"); + (warning_fn "-install set more than once."); let install = match d with | "user" -> UserInstall | "none" -> NoInstall @@ -197,7 +193,7 @@ let process_cmd_line orig_dir proj args = let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match proj.project_file with | None -> () - | Some _ -> warning "Multiple project files are deprecated.@\n%!" + | Some _ -> warning_fn "Multiple project files are deprecated." in parsing_project_file := true; let proj = aux { proj with project_file = Some file } (parse file) in @@ -236,11 +232,11 @@ let process_cmd_line orig_dir proj args = (******************************* API ************************************) -let cmdline_args_to_project ~curdir args = - process_cmd_line curdir (mk_project None None None true) args +let cmdline_args_to_project ~warning_fn ~curdir args = + process_cmd_line ~warning_fn curdir (mk_project None None None true) args -let read_project_file f = - process_cmd_line (Filename.dirname f) +let read_project_file ~warning_fn f = + process_cmd_line ~warning_fn (Filename.dirname f) (mk_project (Some f) None (Some NoInstall) true) (parse f) let rec find_project_file ~from ~projfile_name = |