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

---
 kernel/nativecode.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c19b883e3d..d517d215ed 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -24,6 +24,11 @@ open Environ
 compiler. mllambda represents a fragment of ML, and can easily be printed
 to OCaml code. *)
 
+let debug_native_flag, debug_native_compiler = CDebug.create_full ~name:"native-compiler" ()
+
+let keep_debug_files () =
+  CDebug.get_flag debug_native_flag
+
 (** Local names **)
 
 (* The first component is there for debugging purposes only *)
@@ -1939,7 +1944,7 @@ let compile_constant env sigma con cb =
     | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
-      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
+      debug_native_compiler (fun () -> Pp.str "Generated lambda code");
       let is_lazy = is_lazy t in
       let code = if is_lazy then mk_lazy code else code in
       let l = Constant.label con in
@@ -1950,11 +1955,11 @@ let compile_constant env sigma con cb =
           let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
           (auxdefs,mkMLlam [|univ|] code)
       in
-      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code");
+      debug_native_compiler (fun () -> Pp.str "Generated mllambda code");
       let code =
         optimize_stk (Glet(Gconstant ("", con),code)::auxdefs)
       in
-      if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
+      debug_native_compiler (fun () -> Pp.str "Optimized mllambda code");
       code
     | _ ->
         let i = push_symbol (SymbConst con) in
-- 
cgit v1.2.3