diff options
Diffstat (limited to 'plugins/ltac/profile_ltac_tactics.ml4')
| -rw-r--r-- | plugins/ltac/profile_ltac_tactics.ml4 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 58e3a3a57..9864ffeb6 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -27,6 +27,12 @@ let tclSHOW_PROFILE ~cutoff = let tclSHOW_PROFILE_TACTIC s = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s)) +let tclRESTART_TIMER s = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s)) + +let tclFINISH_TIMING ?(prefix="Timer") (s : string option) = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s)) + TACTIC EXTEND start_ltac_profiling | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] END @@ -45,6 +51,15 @@ TACTIC EXTEND show_ltac_profile | [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ] END +TACTIC EXTEND restart_timer +| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ] +END + +TACTIC EXTEND finish_timing +| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ] +| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ] +END + VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ] END |