From 7ba82ed9f595c7d93bd40846993c2447572a817a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 2 Nov 2016 15:54:37 +0100 Subject: Put string between quotes when printing an option value. This is a better (more generic) fix to #5061 than my e8b9ee76. --- library/goptions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library/goptions.ml') diff --git a/library/goptions.ml b/library/goptions.ml index 35616558a..dfb3c0e69 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -381,9 +381,9 @@ let msg_option_value (name,v) = | BoolValue false -> str "off" | IntValue (Some n) -> int n | IntValue None -> str "undefined" - | StringValue s -> str s + | StringValue s -> str "\"" ++ str s ++ str "\"" | StringOptValue None -> str"undefined" - | StringOptValue (Some s) -> str s + | StringOptValue (Some s) -> str "\"" ++ str s ++ str "\"" (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = -- cgit v1.2.3 From 2c5eef988f11979175de6d1983bc533ce18b1095 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 2 Nov 2016 15:57:19 +0100 Subject: Fix various shortcomings of the warnings infrastructure. - The flags are now interpreted from left to right, without any other precedence rule. The previous one did not make much sense in interactive mode. - Set Warnings and Set Warnings Append are now synonyms, and have the "append" semantics, which is the most natural one for warnings. - Warnings on unknown warnings are now printed only once (previously the would be repeated on further calls to Set Warnings, sections closing, module requiring...). - Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced to "-foo" (if foo exists, "" otherwise). --- lib/cWarnings.ml | 116 +++++++++++++++++++++++++++++++++++----------- lib/cWarnings.mli | 23 ++------- library/goptions.ml | 7 +-- library/goptions.mli | 14 ++++-- parsing/g_vernac.ml4 | 13 ++++-- toplevel/vernacentries.ml | 2 +- 6 files changed, 118 insertions(+), 57 deletions(-) (limited to 'library/goptions.ml') diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 720f54606..68664d1ab 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -21,7 +21,7 @@ let warnings : (string, t) Hashtbl.t = Hashtbl.create 97 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97 let current_loc = ref Loc.ghost -let flags = ref "default" +let flags = ref "" let set_current_loc = (:=) current_loc @@ -62,7 +62,7 @@ let set_warning_status ~name status = try let w = Hashtbl.find warnings name in Hashtbl.replace warnings name { w with status = status } - with Not_found -> warn_unknown_warning name + with Not_found -> () let reset_default_warnings () = Hashtbl.iter (fun name w -> @@ -74,6 +74,13 @@ let set_all_warnings_status status = Hashtbl.replace warnings name { w with status }) warnings +let set_category_status ~name status = + let names = Hashtbl.find categories name in + List.iter (fun name -> set_warning_status name status) names + +let is_all_keyword name = CString.equal name "all" +let is_none_keyword s = CString.equal s "none" + let parse_flag s = if String.length s > 1 then match String.get s 0 with @@ -82,39 +89,94 @@ let parse_flag s = | _ -> (Enabled, s) else CErrors.error "Invalid warnings flag" -let rec do_all_keyword = function - | [] -> [] - | (status, name as item) :: items -> - if CString.equal name "all" then - (set_all_warnings_status status; do_all_keyword items) - else item :: do_all_keyword items - -let rec do_categories = function - | [] -> [] - | (status, name as item) :: items -> - try - let names = Hashtbl.find categories name in - List.iter (fun name -> set_warning_status name status) names; - do_categories items - with Not_found -> item :: do_categories items +let string_of_flag (status,name) = + match status with + | AsError -> "+" ^ name + | Disabled -> "-" ^ name + | Enabled -> name + +let string_of_flags flags = + String.concat "," (List.map string_of_flag flags) + +let set_status ~name status = + if is_all_keyword name then + set_all_warnings_status status + else + try + set_category_status ~name status + with Not_found -> + try + set_warning_status ~name status + with Not_found -> () + +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 + | [] -> acc + | (_status,name as w) :: warnings -> + cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings + +let cut_before_all_rev warnings = cut_before_all_rev [] warnings + +(** [uniquize_flags_rev] removes flags that are subsumed by later occurrences of + themselves or their categories, and reverses the list. *) +let uniquize_flags_rev flags = + let rec aux acc visited = function + | (_,name as flag)::flags -> + if CString.Set.mem name visited then aux acc visited flags else + let visited = + try + let warnings = Hashtbl.find categories name in + CString.Set.union visited (CString.Set.of_list warnings) + with Not_found -> + visited + in + aux (flag::acc) (CString.Set.add name visited) 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. *) +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 + +let flags_of_string s = List.map parse_flag (split_flags s) + +let normalize_flags_string s = + if is_none_keyword s then s + else + let flags = flags_of_string s in + let flags = normalize_flags ~silent:false flags in + string_of_flags flags let rec parse_warnings items = - List.iter (fun (status, name) -> set_warning_status ~name status) items + CList.iter (fun (status, name) -> set_status ~name status) items (* For compatibility, we accept "none" *) -let parse_flags s = - if CString.equal s "none" then begin +let parse_flags s = + if is_none_keyword s then begin Flags.make_warn false; - set_all_warnings_status Disabled + set_all_warnings_status Disabled; + "none" end else begin Flags.make_warn true; - let reg = Str.regexp "[ ,]+" in - let items = List.map parse_flag (Str.split reg s) in - let items = do_all_keyword items in - let items = do_categories items in - parse_warnings items + let flags = flags_of_string s in + let flags = normalize_flags ~silent:true flags in + parse_warnings flags; + string_of_flags flags end let set_flags s = - flags := s; reset_default_warnings (); parse_flags s + reset_default_warnings (); let s = parse_flags s in flags := s diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index 351554284..3f6cee31b 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -6,29 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type status = - Disabled | Enabled | AsError - -(* -type 'a repr = { - print : 'a -> Pp.std_ppcmds; - kind : string; - enabled : bool; -} - *) +type status = Disabled | Enabled | AsError val set_current_loc : Loc.t -> unit val create : name:string -> category:string -> ?default:status -> ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit -(* -val emit : 'a t -> 'a -> unit - -type any = Any : string * string * 'a repr -> any - -val dump : unit -> any list - *) - val get_flags : unit -> string val set_flags : string -> unit + +(** Cleans up a user provided warnings status string, e.g. removing unknown + warnings (in which case a warning is emitted) or subsumed warnings . *) +val normalize_flags_string : string -> string diff --git a/library/goptions.ml b/library/goptions.ml index dfb3c0e69..9dc0f4058 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -247,7 +247,7 @@ let get_locality = function | Some false -> OptGlobal | None -> OptDefault -let declare_option cast uncast append +let declare_option cast uncast append ?(preprocess = fun x -> x) { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in @@ -275,10 +275,11 @@ let declare_option cast uncast append subst_function = subst_options; discharge_function = discharge_options; classify_function = classify_options } in - (fun l m v -> Lib.add_anonymous_leaf (options (l, m, v))) + (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v))) else (fun _ m v -> - match m with + let v = preprocess v in + match m with | OptSet -> write v | OptAppend -> write (append (read ()) v)) in diff --git a/library/goptions.mli b/library/goptions.mli index ca2df0710..3b3651f39 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -122,13 +122,19 @@ type 'a option_sig = { (** When an option is declared synchronous ([optsync] is [true]), the output is a synchronous write function. Otherwise it is [optwrite] *) +(** The [preprocess] function is triggered before setting the option. It can be + used to emit a warning on certain values, and clean-up the final value. *) type 'a write_function = 'a -> unit -val declare_int_option : int option option_sig -> int option write_function -val declare_bool_option : bool option_sig -> bool write_function -val declare_string_option: string option_sig -> string write_function -val declare_stringopt_option: string option option_sig -> string option write_function +val declare_int_option : ?preprocess:(int option -> int option) -> + int option option_sig -> int option write_function +val declare_bool_option : ?preprocess:(bool -> bool) -> + bool option_sig -> bool write_function +val declare_string_option: ?preprocess:(string -> string) -> + string option_sig -> string write_function +val declare_stringopt_option: ?preprocess:(string option -> string option) -> + string option option_sig -> string option write_function (** {6 Special functions supposed to be used only in vernacentries.ml } *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e0d836df8..a33e7257a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -866,11 +866,16 @@ GEXTEND Gram | "Set"; table = option_table; v = option_value -> begin match v with | StringValue s -> - let (last, prefix) = List.sep_last table in - if String.equal last "Append" && not (List.is_empty prefix) then - VernacSetAppendOption (prefix, s) + (* We make a special case for warnings because appending is their + natural semantics *) + if CString.List.equal table ["Warnings"] then + VernacSetAppendOption (table, s) else - VernacSetOption (table, v) + let (last, prefix) = List.sep_last table in + if String.equal last "Append" && not (List.is_empty prefix) then + VernacSetAppendOption (prefix, s) + else + VernacSetOption (table, v) | _ -> VernacSetOption (table, v) end | "Set"; table = option_table -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4de1d9595..c03f183ff 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1491,7 +1491,7 @@ let _ = optwrite = (fun b -> Constrintern.parsing_explicit := b) } let _ = - declare_string_option + declare_string_option ~preprocess:CWarnings.normalize_flags_string { optsync = true; optdepr = false; optname = "warnings display"; -- cgit v1.2.3