[flags] Deprecate is_silent/is_verbose in favor of single flag.

Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.

We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.

2 files changed, 19 insertions, 13 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index d87d9e729..00f515b5a 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 c5c4a15aa..0b00ac13c 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