diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/control.ml | 5 | ||||
| -rw-r--r-- | lib/control.mli | 5 | ||||
| -rw-r--r-- | lib/coqProject_file.ml4 | 15 |
3 files changed, 20 insertions, 5 deletions
diff --git a/lib/control.ml b/lib/control.ml index e67cd8b38d..3fbeb168c4 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -85,4 +85,7 @@ let timeout_fun = match Sys.os_type with | "Unix" | "Cygwin" -> { timeout = unix_timeout } | _ -> { timeout = windows_timeout } -let timeout n f e = timeout_fun.timeout n f e +let timeout_fun_ref = ref timeout_fun +let set_timeout f = timeout_fun_ref := f + +let timeout n f e = !timeout_fun_ref.timeout n f e diff --git a/lib/control.mli b/lib/control.mli index 415e054625..59e2a15158 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -24,3 +24,8 @@ val check_for_interrupt : unit -> unit val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b (** [timeout n f x e] tries to compute [f x], and if it fails to do so before [n] seconds, it raises [e] instead. *) + +(** Set a particular timeout function; warning, this is an internal + API and it is scheduled to go away. *) +type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } +val set_timeout : timeout -> unit diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index d6c340f691..61eb1dafdf 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -8,6 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* This needs to go trou feedback as it is invoked from IDEs, but + 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 } @@ -122,7 +130,7 @@ let process_cmd_line orig_dir proj args = 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 *) if orig_dir = "." then "" else orig_dir in - let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in + let error s = (Format.eprintf "Error: @[%s@].@\n%!" s; exit 1) in let mk_path d = let p = CUnix.correct_path d orig_dir in { path = CUnix.remove_path_dot (post_canonize p); @@ -140,7 +148,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 - Feedback.msg_warning (Pp.str "-install set more than once."); + (warning "-install set more than once.@\n%!"); let install = match d with | "user" -> UserInstall | "none" -> NoInstall @@ -167,8 +175,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 _ -> Feedback.msg_warning (Pp.str - "Multiple project files are deprecated.") + | Some _ -> warning "Multiple project files are deprecated.@\n%!" in parsing_project_file := true; let proj = aux { proj with project_file = Some file } (parse file) in |