From 068031ff7da092c1e2d35db27d713b9606960c42 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Oct 2020 15:31:51 +0200
Subject: Infrastructure for fine-grained debug flags

---
 vernac/proof_using.ml   | 17 +++++++++--------
 vernac/vernacentries.ml | 13 ++++++++++---
 2 files changed, 19 insertions(+), 11 deletions(-)

(limited to 'vernac')

diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index bdb0cabacf..d859fcafe2 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -91,13 +91,14 @@ let remove_ids_and_lets env s ids =
 let record_proof_using expr =
   Aux_file.record_in_aux "suggest_proof_using" expr
 
+let debug_proof_using = CDebug.create ~name:"proof-using" ()
+
 (* Variables in [skip] come from after the definition, so don't count
    for "All". Used in the variable case since the env contains the
    variable itself. *)
 let suggest_common env ppid used ids_typ skip =
   let module S = Id.Set in
   let open Pp in
-  let print x = Feedback.msg_debug x in
   let pr_set parens s =
     let wrap ppcmds =
       if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
@@ -111,13 +112,13 @@ let suggest_common env ppid used ids_typ skip =
   in
   let all = S.diff all skip in
   let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in
-  if !Flags.debug then begin
-    print (str "All "        ++ pr_set false all);
-    print (str "Type "       ++ pr_set false ids_typ);
-    print (str "needed "     ++ pr_set false needed);
-    print (str "all_needed " ++ pr_set false all_needed);
-    print (str "Type* "      ++ pr_set false fwd_typ);
-  end;
+  let () = debug_proof_using (fun () ->
+      str "All "        ++ pr_set false all ++ fnl() ++
+      str "Type "       ++ pr_set false ids_typ ++ fnl() ++
+      str "needed "     ++ pr_set false needed ++ fnl() ++
+      str "all_needed " ++ pr_set false all_needed ++ fnl() ++
+      str "Type* "      ++ pr_set false fwd_typ)
+  in
   let valid_exprs = ref [] in
   let valid e = valid_exprs := e :: !valid_exprs in
   if S.is_empty needed then valid (str "Type");
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 42ba63903d..c38cfbadc2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1644,6 +1644,13 @@ let () =
       optread  = CWarnings.get_flags;
       optwrite = CWarnings.set_flags }
 
+let () =
+  declare_string_option
+    { optdepr  = false;
+      optkey   = ["Debug"];
+      optread  = CDebug.get_flags;
+      optwrite = CDebug.set_flags }
+
 let () =
   declare_bool_option
     { optdepr  = false;
@@ -1710,9 +1717,9 @@ let vernac_set_append_option ~locality key s =
 
 let vernac_set_option ~locality table v = match v with
 | OptionSetString s ->
-  (* We make a special case for warnings because appending is their
-  natural semantics *)
-  if CString.List.equal table ["Warnings"] then
+  (* We make a special case for warnings and debug flags because appending is
+  their natural semantics *)
+  if CString.List.equal table ["Warnings"] || CString.List.equal table ["Debug"] then
     vernac_set_append_option ~locality table s
   else
     let (last, prefix) = List.sep_last table in
-- 
cgit v1.2.3