diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/backtrace.ml | 1 | ||||
| -rw-r--r-- | lib/cErrors.ml | 2 | ||||
| -rw-r--r-- | lib/cWarnings.ml | 4 | ||||
| -rw-r--r-- | lib/feedback.ml | 2 | ||||
| -rw-r--r-- | lib/flags.ml | 16 | ||||
| -rw-r--r-- | lib/flags.mli | 16 | ||||
| -rw-r--r-- | lib/stateid.ml | 1 |
7 files changed, 24 insertions, 18 deletions
diff --git a/lib/backtrace.ml b/lib/backtrace.ml index b3b8bdea2e..be9f40c1fb 100644 --- a/lib/backtrace.ml +++ b/lib/backtrace.ml @@ -5,6 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +[@@@ocaml.warning "-37"] type raw_frame = | Known_location of bool (* is_raise *) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 1c1ff7e2fd..b55fd80c68 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -121,12 +121,14 @@ end by inner functions during a [vernacinterp]. They should be handled only at the very end of interp, to be displayed to the user. *) +[@@@ocaml.warning "-52"] let noncritical = function | Sys.Break | Out_of_memory | Stack_overflow | Assert_failure _ | Match_failure _ | Anomaly _ | Timeout | Drop | Quit -> false | Invalid_argument "equal: functional value" -> false | _ -> true +[@@@ocaml.warning "+52"] (** Check whether an exception is handled *) diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 2f569d2849..71e02b3ba4 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -82,7 +82,7 @@ let set_all_warnings_status status = let set_category_status ~name status = let names = Hashtbl.find categories name in - List.iter (fun name -> set_warning_status name status) names + 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" @@ -166,7 +166,7 @@ let normalize_flags_string s = let flags = normalize_flags ~silent:false flags in string_of_flags flags -let rec parse_warnings items = +let parse_warnings items = CList.iter (fun (status, name) -> set_status ~name status) items (* For compatibility, we accept "none" *) diff --git a/lib/feedback.ml b/lib/feedback.ml index df6fe3a629..0846e419b2 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -40,8 +40,6 @@ type feedback = { contents : feedback_content; } -let default_route = 0 - (** Feeders *) let feeders : (int, feedback -> unit) Hashtbl.t = Hashtbl.create 7 diff --git a/lib/flags.ml b/lib/flags.ml index d87d9e7295..00f515b5a6 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -143,16 +143,16 @@ let beautify = ref false let beautify_file = ref false (* Silent / Verbose *) -let silent = ref false -let make_silent flag = silent := flag; () -let is_silent () = !silent -let is_verbose () = not !silent +let quiet = ref false +let silently f x = with_option quiet f x +let verbosely f x = without_option quiet f x -let silently f x = with_option silent f x -let verbosely f x = without_option silent f x +let if_silent f x = if !quiet then f x +let if_verbose f x = if not !quiet then f x -let if_silent f x = if !silent then f x -let if_verbose f x = if not !silent then f x +let make_silent flag = quiet := flag +let is_silent () = !quiet +let is_verbose () = not !quiet let auto_intros = ref true let make_auto_intros flag = auto_intros := flag diff --git a/lib/flags.mli b/lib/flags.mli index c5c4a15aaa..0b00ac13c2 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -85,16 +85,22 @@ val pr_version : compat_version -> string val beautify : bool ref val beautify_file : bool ref -(* Silent/verbose, both actually controlled by a single flag so they - are mutually exclusive *) -val make_silent : bool -> unit -val is_silent : unit -> bool -val is_verbose : unit -> bool +(* Coq quiet mode. Note that normal mode is called "verbose" here, + whereas [quiet] supresses normal output such as goals in coqtop *) +val quiet : bool ref val silently : ('a -> 'b) -> 'a -> 'b val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit +(* Deprecated *) +val make_silent : bool -> unit +[@@ocaml.deprecated "Please use Flags.quiet"] +val is_silent : unit -> bool +[@@ocaml.deprecated "Please use Flags.quiet"] +val is_verbose : unit -> bool +[@@ocaml.deprecated "Please use Flags.quiet"] + (* Miscellaneus flags for vernac *) val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool diff --git a/lib/stateid.ml b/lib/stateid.ml index ae25735c5f..c153f0e808 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -32,7 +32,6 @@ let compare = Int.compare module Self = struct type t = int let compare = compare - let equal = equal end module Set = Set.Make(Self) |