From db2be6c46d3882cadea3a14311d3ce7e21c53b83 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Mon, 30 Oct 2000 16:58:32 +0000
Subject: Ajout d'un switch pour le debugger

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@790 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 16 +++++++++++++++-
 toplevel/vernacinterp.ml  |  2 +-
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index afe871641e..8d109ab7ed 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -27,6 +27,8 @@ open Ast
 open Astterm
 open Pretty
 open Printer
+open Tacinterp
+open Tactic_debug
 open Command
 
 (* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *)
@@ -663,6 +665,18 @@ let _ =
        | [] -> (fun () -> make_silent false)
        | _  -> bad_vernac_args "EndSilent")
 
+let _ =
+  add "DebugOn"
+    (function 
+       | [] -> (fun () -> set_debug DebugOn)
+       | _  -> bad_vernac_args "DebugOn")
+
+let _ =
+  add "DebugOff"
+    (function 
+       | [] -> (fun () -> set_debug DebugOff)
+       | _  -> bad_vernac_args "DebugOff")
+
 let _ =
   add "StartProof"
     (function 
@@ -1205,7 +1219,7 @@ let _ =
     (let rec tacdef_fun lacc=function
         (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl ->
           let ve=
-            Tacinterp.val_interp (empty,empty_env,[],[],None) tacexp
+            val_interp (empty,empty_env,[],[],None,get_debug ()) tacexp
           in
             tacdef_fun ((string_of_id name,ve)::lacc) tl
        |[] ->
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 5308efba17..602818ccd0 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -97,7 +97,7 @@ let rec cvt_varg ast =
     | Node(_,"ASTLIST",al) -> VARG_ASTLIST al
     | Node(_,"TACTIC_ARG",[targ]) ->
       let (evc,env)= Command.get_current_context () in
-      VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None) targ)
+      VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None,get_debug ()) targ)
     | Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d
     | _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg",
                         [< 'sTR "Unrecognizable ast node of vernac arg:";
-- 
cgit v1.2.3