diff options
| -rw-r--r-- | parsing/g_vernac.ml4 | 7 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 15 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
3 files changed, 16 insertions, 7 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 68ef987498..737c97bae3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -652,8 +652,11 @@ GEXTEND Gram VernacBacktrack (n,m,p) (* Tactic Debugger *) - | IDENT "Debug"; IDENT "On" -> VernacDebug true - | IDENT "Debug"; IDENT "Off" -> VernacDebug false + | IDENT "Debug"; IDENT "On" -> + VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue true) + + | IDENT "Debug"; IDENT "Off" -> + VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue false) ] ]; END diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 42f7ec71b8..5c0ac05f0c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -789,6 +789,17 @@ let _ = optread=Pp_control.get_margin; optwrite=Pp_control.set_margin } +let vernac_debug b = + set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) + +let _ = + declare_bool_option + { optsync=false; + optkey=SecondaryTable("Ltac","Debug"); + optname="Ltac debug"; + optread=(fun () -> get_debug () <> Tactic_debug.DebugOff); + optwrite=vernac_debug } + let vernac_set_opacity opaq locqid = match Nametab.global locqid with | ConstRef sp -> @@ -1069,9 +1080,6 @@ let vernac_check_guard () = in msgnl message -let vernac_debug b = - set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) - let interp c = match c with (* Control (done in vernac) *) | (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false @@ -1175,7 +1183,6 @@ let interp c = match c with | VernacGo g -> vernac_go g | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacDebug b -> vernac_debug b | VernacProof tac -> vernac_set_end_tac tac (* Toplevel control *) | VernacToplevelControl e -> raise e diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 0ba2610c4b..51010afa80 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -281,7 +281,6 @@ type vernac_expr = | VernacGo of goable | VernacShow of showable | VernacCheckGuard - | VernacDebug of bool | VernacProof of raw_tactic_expr (* Toplevel control *) | VernacToplevelControl of exn |