From f63c0cdd3c7da642e505569e83199784bbfdc367 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 28 May 2015 19:00:07 +0200 Subject: 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) --- toplevel/vernac.ml | 10 +++++----- 1 file 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 -- cgit v1.2.3