[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.

14 files changed, 40 insertions, 34 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
diff --git a/library/loadpath.ml b/library/loadpath.ml
index d03c6c555..529b9502b 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -113,5 +113,5 @@ let expand_path ?root dir =
 let locate_file fname =
   let paths = List.map physical !load_paths in
   let _,longfname =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+    System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in
   longfname
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 92d249e53..dad98e2e9 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -211,7 +211,7 @@ let camlp4_verbosity silent f x =
   f x;
   warning_verbose := a
 
-let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
+let camlp4_verbose f x = camlp4_verbosity (not !Flags.quiet) f x
 
 (** Grammar extensions *)
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5460d6fb7..9788ccfee 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1590,8 +1590,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       and eq_ref = destConst (constr_of_global eq_ref) in
       generate_induction_principle f_ref tcc_lemma_constr
 	functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation);
-      if Flags.is_verbose ()
-      then msgnl (h 1 (Ppconstr.pr_id function_name ++
+      Flags.if_verbose
+        msgnl (h 1 (Ppconstr.pr_id function_name ++
 			 spc () ++ str"is defined" )++ fnl () ++
 		    h 1 (Ppconstr.pr_id equation_id ++
 			   spc () ++ str"is defined" )
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 632ba0d9c..e9b3d197b 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -388,7 +388,7 @@ let add_coercion_in_graph (ic,source,target) =
       old_inheritance_graph
   end;
   let is_ambig = match !ambig_paths with [] -> false | _ -> true in
-  if is_ambig && is_verbose () then
+  if is_ambig && not !quiet then
     Feedback.msg_info (message_ambig !ambig_paths)
 
 type coercion = {
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
index 50b42512c..86ef59dc3 100644
--- a/stm/workerLoop.ml
+++ b/stm/workerLoop.ml
@@ -13,7 +13,7 @@ let rec parse = function
 
 let loop init args =
   let args = parse args in
-  Flags.make_silent true;
+  Flags.quiet := true;
   init ();
   CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
   args
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ea1966093..df222eed8 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -590,7 +590,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
 				       info.Vernacexpr.hint_pattern }
 	      in
 	      make_resolves env sigma ~name:(PathHints path)
-                  (true,false,Flags.is_verbose()) info false
+                  (true,false,not !Flags.quiet) info false
                  (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
                hints)
         else []
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 77ed4330c..bcc068d3d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1160,7 +1160,7 @@ let add_resolves env sigma clist local dbnames =
     (fun dbname ->
       let r =
         List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
-          make_resolves env sigma (true,hnf,Flags.is_verbose()) 
+          make_resolves env sigma (true,hnf,not !Flags.quiet)
             pri poly ~name:path gr) clist)
       in
       let hint = make_hint ~local dbname (AddHints r) in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c259beb17..18a38525d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -215,7 +215,7 @@ let glob_opt = ref false
 
 let add_compile verbose s =
   set_batch_mode ();
-  Flags.make_silent true;
+  Flags.quiet := true;
   if not !glob_opt then Dumpglob.dump_to_dotglob ();
   (** make the file name explicit; needed not to break up Coq loadpath stuff. *)
   let s =
@@ -384,7 +384,7 @@ let vio_tasks = ref []
 
 let add_vio_task f =
   set_batch_mode ();
-  Flags.make_silent true;
+  Flags.quiet := true;
   vio_tasks := f :: !vio_tasks
 
 let check_vio_tasks () =
@@ -398,7 +398,7 @@ let vio_files_j = ref 0
 let vio_checking = ref false
 let add_vio_file f =
   set_batch_mode ();
-  Flags.make_silent true;
+  Flags.quiet := true;
   vio_files := f :: !vio_files
 
 let set_vio_checking_j opt j =
@@ -563,7 +563,7 @@ let parse_args arglist =
     |"-output-context" -> output_context := true
     |"-profile-ltac" -> Flags.profile_ltac := true
     |"-q" -> no_load_rc ()
-    |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false
+    |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
     |"-quick" -> Flags.compilation_mode := BuildVio
     |"-list-tags" -> print_tags := true
     |"-time" -> Flags.time := true
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 18f93197c..fd208bd89 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -116,7 +116,7 @@ let rec interp_vernac sid po (loc,com) =
         load_vernac verbosely sid f
     | v ->
       try
-        let nsid, ntip = Stm.add sid (Flags.is_verbose()) (loc,v) in
+        let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in
 
         (* Main STM interaction *)
         if ntip <> `NewTip then
@@ -128,7 +128,7 @@ let rec interp_vernac sid po (loc,com) =
 
         (* We could use a more refined criteria that depends on the
            vernac. For now we imitate the old approach. *)
-        let hide_goals = !Flags.batch_mode || is_query v ||
+        let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet ||
                          not (Proof_global.there_are_pending_proofs ()) in
 
         if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
diff --git a/vernac/command.ml b/vernac/command.ml
index 5ec708446..45ff57955 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -234,7 +234,7 @@ match local with
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
   let () =
-    if is_verbose () && Pfedit.refining () then
+    if not !Flags.quiet && Pfedit.refining () then
     Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++
     strbrk " is not visible from current goals")
   in
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 2396cf04a..056ffca5c 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -138,7 +138,7 @@ let dir_ml_load s =
   match !load with
     | WithTop _ -> ml_load s
     | WithoutTop ->
-        let warn = Flags.is_verbose() in
+        let warn = not !Flags.quiet in
         let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
         ml_load gname
 
@@ -365,7 +365,7 @@ let trigger_ml_object verb cache reinit ?path name =
   else begin
     let file = file_of_name (Option.default name path) in
     let path =
-      if_verbose_load (verb && is_verbose ()) load_ml_object name ?path file in
+      if_verbose_load (verb && not !quiet) load_ml_object name ?path file in
     add_loaded_module name (Some path);
     if cache then perform_cache_obj name
   end
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 92b1a5956..c50c27c45 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -780,7 +780,7 @@ let vernac_require from import qidl =
   in
   let locate (loc, qid) =
     try
-      let warn = Flags.is_verbose () in
+      let warn = not !Flags.quiet in
       let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
       (dir, f)
     with
@@ -1232,8 +1232,8 @@ let _ =
       optdepr  = false;
       optname  = "silent";
       optkey   = ["Silent"];
-      optread  = is_silent;
-      optwrite = make_silent }
+      optread  = (fun () -> !Flags.quiet);
+      optwrite = ((:=) Flags.quiet) }
 
 let _ =
   declare_bool_option
@@ -2173,7 +2173,7 @@ let with_fail b f =
       | HasNotFailed ->
           user_err ~hdr:"Fail" (str "The command has not failed!")
       | HasFailed msg ->
-          if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info
+          if not !Flags.quiet || !test_mode || !ide_slave then Feedback.msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end