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 /ide | |
| 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 'ide')
| -rw-r--r-- | ide/coqide.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index a26f7d1b94..b3160174ad 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -103,7 +103,8 @@ let make_coqtop_args fname = with | None -> "", base_args | Some proj -> - proj, coqtop_args_from_project (read_project_file proj) @ base_args + let warning_fn x = Feedback.msg_warning Pp.(str x) in + proj, coqtop_args_from_project (read_project_file ~warning_fn proj) @ base_args in let args = match fname with | None -> args @@ -112,7 +113,6 @@ let make_coqtop_args fname = else "-topfile"::fname::args in proj, args -;; (** Setting drag & drop on widgets *) @@ -1355,7 +1355,8 @@ let read_coqide_args argv = 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 = CoqProject_file.read_project_file file in + let warning_fn x = Format.eprintf "%s@\n%!" x in + let p = CoqProject_file.read_project_file ~warning_fn file in filter_coqtop coqtop (Some (d,p)) out args |"-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 |