diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cWarnings.ml | 21 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 4 | ||||
| -rw-r--r-- | lib/future.ml | 2 |
4 files changed, 10 insertions, 19 deletions
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 0cf989e494..f199e2e608 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp - type status = Disabled | Enabled | AsError @@ -158,6 +156,10 @@ let set_flags s = warning flags string, because the warning being created might have been set already. *) let create ~name ~category ?(default=Enabled) pp = + let pp x = let open Pp in + pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ + str category ++ str "]" + in Hashtbl.replace warnings name { default; category; status = default }; add_warning_in_category ~name ~category; if default <> Disabled then @@ -166,13 +168,8 @@ let create ~name ~category ?(default=Enabled) pp = new warning is now known. *) set_flags !flags; fun ?loc x -> - let w = Hashtbl.find warnings name in - match w.status with - | Disabled -> () - | AsError -> CErrors.user_err ?loc (pp x) - | Enabled -> - let msg = - pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ - str category ++ str "]" - in - Feedback.msg_warning ?loc msg + let w = Hashtbl.find warnings name in + match w.status with + | Disabled -> () + | AsError -> CErrors.user_err ?loc (pp x) + | Enabled -> Feedback.msg_warning ?loc (pp x) diff --git a/lib/flags.ml b/lib/flags.ml index 1195b8caf1..6718e7a954 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -43,8 +43,6 @@ let with_options ol f x = let record_aux_file = ref false -let test_mode = ref false - let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = !async_proofs_worker_id <> "master" diff --git a/lib/flags.mli b/lib/flags.mli index 2b4446a1db..bf8846417b 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -35,10 +35,6 @@ be eventually removed by cleanups such as PR#1103 *) val record_aux_file : bool ref -(* Flag set when the test-suite is called. Its only effect to display - verbose information for `Fail` *) -val test_mode : bool ref - (** Async-related flags *) val async_proofs_worker_id : string ref val async_proofs_is_worker : unit -> bool diff --git a/lib/future.ml b/lib/future.ml index b372bedc5d..6e7c6fd9e3 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -33,7 +33,7 @@ let _ = CErrors.register_handler (function | _ -> raise CErrors.Unhandled) type fix_exn = Exninfo.iexn -> Exninfo.iexn -let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument. You probably want to chain with an already existing future instead."; x +let id x = x module UUID = struct type t = int |