From b6733f0507e3e04fb6130b3f82a79e8835e1062f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 31 May 2017 00:30:00 +0200 Subject: Bump year in headers. --- lib/aux_file.ml | 2 +- lib/aux_file.mli | 2 +- lib/bigint.ml | 2 +- lib/bigint.mli | 2 +- lib/cEphemeron.ml | 2 +- lib/cEphemeron.mli | 2 +- lib/cMap.ml | 2 +- lib/cMap.mli | 2 +- lib/cSet.ml | 2 +- lib/cSet.mli | 2 +- lib/cString.ml | 2 +- lib/cString.mli | 2 +- lib/cThread.ml | 2 +- lib/cThread.mli | 2 +- lib/cUnix.ml | 2 +- lib/cUnix.mli | 2 +- lib/cWarnings.ml | 2 +- lib/cWarnings.mli | 2 +- lib/canary.ml | 2 +- lib/canary.mli | 2 +- lib/control.ml | 2 +- lib/control.mli | 2 +- lib/deque.ml | 2 +- lib/deque.mli | 2 +- lib/dyn.ml | 2 +- lib/dyn.mli | 2 +- lib/envars.ml | 2 +- lib/envars.mli | 2 +- lib/explore.ml | 2 +- lib/explore.mli | 2 +- lib/feedback.ml | 2 +- lib/feedback.mli | 2 +- lib/flags.ml | 2 +- lib/flags.mli | 2 +- lib/future.ml | 2 +- lib/future.mli | 2 +- lib/genarg.ml | 2 +- lib/genarg.mli | 2 +- lib/hMap.ml | 2 +- lib/hMap.mli | 2 +- lib/hashcons.ml | 2 +- lib/hashcons.mli | 2 +- lib/hashset.ml | 2 +- lib/hashset.mli | 2 +- lib/heap.ml | 2 +- lib/heap.mli | 2 +- lib/hook.ml | 2 +- lib/hook.mli | 2 +- lib/iStream.ml | 2 +- lib/iStream.mli | 2 +- lib/int.ml | 2 +- lib/int.mli | 2 +- lib/loc.ml | 2 +- lib/loc.mli | 2 +- lib/minisys.ml | 2 +- lib/option.ml | 2 +- lib/option.mli | 2 +- lib/pp.ml | 2 +- lib/pp.mli | 2 +- lib/pp_control.ml | 2 +- lib/pp_control.mli | 2 +- lib/ppstyle.ml | 2 +- lib/ppstyle.mli | 2 +- lib/profile.ml | 2 +- lib/profile.mli | 2 +- lib/remoteCounter.ml | 2 +- lib/remoteCounter.mli | 2 +- lib/richpp.ml | 2 +- lib/richpp.mli | 2 +- lib/rtree.ml | 2 +- lib/rtree.mli | 2 +- lib/spawn.ml | 2 +- lib/spawn.mli | 2 +- lib/system.ml | 2 +- lib/system.mli | 2 +- lib/terminal.ml | 2 +- lib/terminal.mli | 2 +- lib/trie.ml | 2 +- lib/trie.mli | 2 +- lib/unicode.mli | 2 +- lib/unionfind.ml | 2 +- lib/unionfind.mli | 2 +- lib/util.mli | 2 +- lib/xml_datatype.mli | 2 +- 84 files changed, 84 insertions(+), 84 deletions(-) (limited to 'lib') diff --git a/lib/aux_file.ml b/lib/aux_file.ml index c6c7b42429..64c687e868 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Some !current_loc - | loc -> loc - -let create ~name ~category ?(default=Enabled) pp = - Hashtbl.add warnings name { default; category; status = default }; - add_warning_in_category ~name ~category; - if default <> Disabled then - add_warning_in_category ~name ~category:"default"; - fun ?loc x -> let w = Hashtbl.find warnings name in - match w.status with - | Disabled -> () - | AsError -> - begin match refine_loc loc with - | Some loc -> CErrors.user_err_loc (loc,"_",pp x) - | None -> CErrors.errorlabstrm "_" (pp x) - end - | Enabled -> - let msg = - pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ - str category ++ str "]" - in - let loc = refine_loc loc in - Feedback.msg_warning ?loc msg - -let warn_unknown_warning = - create ~name:"unknown-warning" ~category:"toplevel" - (fun name -> strbrk "Unknown warning name: " ++ str name) - let set_warning_status ~name status = try let w = Hashtbl.find warnings name in @@ -118,12 +89,6 @@ let set_status ~name status = let split_flags s = let reg = Str.regexp "[ ,]+" in Str.split reg s -let check_warning ~silent (_status,name) = - is_all_keyword name || - Hashtbl.mem categories name || - Hashtbl.mem warnings name || - (if not silent then warn_unknown_warning name; false) - (** [cut_before_all_rev] removes all flags subsumed by a later occurrence of the "all" flag, and reverses the list. *) let rec cut_before_all_rev acc = function @@ -150,10 +115,9 @@ let uniquize_flags_rev flags = | [] -> acc in aux [] CString.Set.empty flags -(** [normalize_flags] removes unknown or redundant warnings. If [silent] is - true, it emits a warning when an unknown warning is met. *) +(** [normalize_flags] removes redundant warnings. Unknown warnings are kept + because they may be declared in a plugin that will be linked later. *) let normalize_flags ~silent warnings = - let warnings = List.filter (check_warning ~silent) warnings in let warnings = cut_before_all_rev warnings in uniquize_flags_rev warnings @@ -186,3 +150,35 @@ let parse_flags s = let set_flags s = reset_default_warnings (); let s = parse_flags s in flags := s + +let refine_loc = function + | None when not (Loc.is_ghost !current_loc) -> Some !current_loc + | loc -> loc + +(* Adds a warning to the [warnings] and [category] tables. We then reparse the + warning flags string, because the warning being created might have been set + already. *) +let create ~name ~category ?(default=Enabled) pp = + Hashtbl.replace warnings name { default; category; status = default }; + add_warning_in_category ~name ~category; + if default <> Disabled then + add_warning_in_category ~name ~category:"default"; + (* We re-parse and also re-normalize the flags, because the category of the + new warning is now known. *) + set_flags !flags; + fun ?loc x -> let w = Hashtbl.find warnings name in + match w.status with + | Disabled -> () + | AsError -> + begin match refine_loc loc with + | Some loc -> CErrors.user_err_loc (loc,"_",pp x) + | None -> CErrors.errorlabstrm "_" (pp x) + end + | Enabled -> + let msg = + pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ + str category ++ str "]" + in + let loc = refine_loc loc in + Feedback.msg_warning ?loc msg + -- cgit v1.2.3