make Unset Silent work in coqc

Trying to untangle the flags:

coqc -verbose coqtop -compile-verbose are used just to print the commands run;
-quiet, -silent, Set Silent, Unset Silent control Flags.verbose flag.

Flags.verbose controls many prints that are expected to be made in
interactive mode.  E.g. "Proof" or "tac" prints goals if such flag is
true.  To flip it, one can "Set/Unset Silent" in both coqtop and coqc
mode.

It is still messy, but the confusion between -verbose and Flags.verbose
has gone (I must have identified the two things with my initial STM
patch)

1 files changed, 5 insertions, 5 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5418c60e9..a06702e0d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -215,7 +215,7 @@ let display_cmd_header loc com =
 	 str " [" ++ str cmd ++ str "] ");
   Pp.flush_all ()
 
-let rec vernac_com verbosely checknav (loc,com) =
+let rec vernac_com checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
@@ -241,7 +241,7 @@ let rec vernac_com verbosely checknav (loc,com) =
 
     | v when !just_parsing -> ()
 
-    | v -> Stm.interp verbosely (loc,v)
+    | v -> Stm.interp (Flags.is_verbose()) (loc,v)
   in
     try
       checknav loc com;
@@ -268,7 +268,7 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
-      vernac_com verbosely checknav loc_ast;
+      vernac_com checknav loc_ast;
       pp_flush ()
     done
   with any ->   (* whatever the exception *)
@@ -292,14 +292,14 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
+let eval_expr loc_ast = vernac_com checknav loc_ast
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
   chan_beautify :=
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
   try
-    read_vernac_file verb file;
+    Flags.silently (read_vernac_file verb) file;
     if !Flags.beautify_file then close_out !chan_beautify;
   with any ->
     let (e, info) = Errors.push any in