[toplevel] Remove duplicate beautify flags.

Given the current style in flags.mli no reason to have a function.

A deeper question is why a global flag is needed, in particular the use
in `interp/constrextern.ml` seems strange, the condition in the lexer
should be looked at and I'm not sure about `printing/`.

7 files changed, 9 insertions, 13 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 65873e5214..35681804fc 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -139,8 +139,6 @@ let pr_version = function
 
 (* Translate *)
 let beautify = ref false
-let make_beautify f = beautify := f
-let do_beautify () = !beautify
 let beautify_file = ref false
 
 (* Silent / Verbose *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 9dc0c9c048..897602641c 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -70,8 +70,6 @@ val version_less_or_equal : compat_version -> bool
 val pr_version : compat_version -> string
 
 val beautify : bool ref
-val make_beautify : bool -> unit
-val do_beautify : unit -> bool
 val beautify_file : bool ref
 
 val make_silent : bool -> unit
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index cfee77ab29..e59b9630fb 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -390,7 +390,7 @@ let comment_stop ep =
   if !Flags.xml_export && Buffer.length current_comment > 0 &&
     (!between_commands || not(null_comment current_s)) then
       Hook.get f_xml_output_comment current_s;
-  (if Flags.do_beautify() && Buffer.length current_comment > 0 &&
+  (if !Flags.beautify && Buffer.length current_comment > 0 &&
     (!between_commands || not(null_comment current_s)) then
     let bp = match !comment_begin with
         Some bp -> bp
@@ -437,7 +437,7 @@ let rec comment loc bp = parser bp2
       let loc =
 	(* In beautify mode, the lexing differs between strings in comments and
 	   regular strings (e.g. escaping). It seems wrong. *)
-	if Flags.do_beautify() then (push_string"\""; comm_string loc bp2 s)
+	if !Flags.beautify then (push_string"\""; comm_string loc bp2 s)
 	else fst (string loc ~comm_level:(Some 0) bp2 0 s)
       in
       comment loc bp s
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index c94650f1ee..aa94fb7be3 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -129,7 +129,7 @@ end) = struct
     str "`" ++ str hd ++ c ++ str tl
 
   let pr_com_at n =
-    if Flags.do_beautify() && not (Int.equal n 0) then comment (CLexer.extract_comments n)
+    if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
     else mt()
 
   let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 57a1d957e0..50ce56fb02 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -9,7 +9,7 @@
 open Pp
 
 let pr_located pr (loc, x) =
-  if Flags.do_beautify () && loc <> Loc.ghost then
+  if !Flags.beautify && loc <> Loc.ghost then
     let (b, e) = Loc.unloc loc in
     (* Side-effect: order matters *)
     let before = Pp.comment (CLexer.extract_comments b) in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 26ef68262b..4fd2b0e92b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -168,7 +168,7 @@ let load_vernacular () =
   List.iter
     (fun (s,b) ->
       let s = Loadpath.locate_file s in
-      if Flags.do_beautify () then
+      if !Flags.beautify then
 	with_option beautify_file (Vernac.load_vernac b) s
       else
 	Vernac.load_vernac b s)
@@ -219,7 +219,7 @@ let add_compile verbose s =
   compile_list := (verbose,s) :: !compile_list
 
 let compile_file (v,f) =
-  if Flags.do_beautify () then
+  if !Flags.beautify then
     with_option beautify_file (Vernac.compile v) f
   else
     Vernac.compile v f
@@ -536,7 +536,7 @@ let parse_args arglist =
         Flags.async_proofs_never_reopen_branch := true;
     |"-batch" -> set_batch_mode ()
     |"-test-mode" -> test_mode := true
-    |"-beautify" -> make_beautify true
+    |"-beautify" -> beautify := true
     |"-boot" -> boot := true; no_load_rc ()
     |"-bt" -> Backtrace.record_backtrace true
     |"-color" -> set_color (next ())
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 54b2ac3c17..8230f92a64 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -199,7 +199,7 @@ let rec interp_vernac po chan_beautify checknav (loc,com) =
   in
     try
       checknav loc com;
-      if do_beautify () then pr_new_syntax po chan_beautify loc (Some com);
+      if !beautify then pr_new_syntax po chan_beautify loc (Some com);
       (* XXX: This is not 100% correct if called from an IDE context *)
       if !Flags.time then print_cmd_header loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
@@ -228,7 +228,7 @@ and load_vernac verbosely file =
     close_input in_chan input;    (* we must close the file first *)
     match e with
       | End_of_input ->
-          if do_beautify () then
+          if !beautify then
             pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None;
           if !Flags.beautify_file then close_out chan_beautify;
       | reraise ->