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

---
 sysinit/coqargs.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'sysinit')

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 56d88e6bd6..8be73ca028 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -21,14 +21,6 @@ let error_missing_arg s =
   prerr_endline "See -help for the syntax of supported options";
   exit 1
 
-(******************************************************************************)
-(* Imperative effects! This must be fixed at some point.                      *)
-(******************************************************************************)
-
-let set_debug () =
-  let () = Exninfo.record_backtrace true in
-  Flags.debug := true
-
 (******************************************************************************)
 
 type native_compiler = Coq_config.native_compiler =
@@ -168,6 +160,9 @@ let add_load_vernacular opts verb s =
 let add_set_option opts opt_name value =
   { opts with pre = { opts.pre with injections = OptionInjection (opt_name, value) :: opts.pre.injections }}
 
+let add_set_debug opts flags =
+  add_set_option opts ["Debug"] (OptionAppend flags)
+
 (** Options for proof general *)
 let set_emacs opts =
   let opts = add_set_option opts Printer.print_goal_tag_opt_name (OptionSet None) in
@@ -382,10 +377,15 @@ let parse_args ~usage ~init arglist : t * string list =
     (* Options with zero arg *)
     |"-test-mode" -> Vernacinterp.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
-    |"-bt" -> Exninfo.record_backtrace true; oval
+    |"-bt" -> add_set_debug oval "backtrace"
     |"-config"|"--config" -> set_query oval PrintConfig
-    |"-debug" -> set_debug (); oval
-    |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval
+
+    |"-debug" -> add_set_debug oval "all"
+    |"-d" | "-D" -> add_set_debug oval (next())
+
+    (* -xml-debug implies -debug. TODO don't be imperative here. *)
+    |"-xml-debug" -> Flags.xml_debug := true; add_set_debug oval "all"
+
     |"-diffs" ->
       add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ()))
     |"-emacs" -> set_emacs oval
-- 
cgit v1.2.3