diff options
| author | Enrico Tassi | 2016-09-28 16:32:42 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-09-29 10:47:00 +0200 |
| commit | e1df1b77f8c72636b6e347f41f6f38976c86e909 (patch) | |
| tree | fc6fb2a6a6f92a8c7e4a1368855de6f112e95836 /ltac | |
| parent | ed53e048fc5e4b995c1e0c42bf1ba1611c331cce (diff) | |
-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/profile_ltac.ml | 4 | ||||
| -rw-r--r-- | ltac/profile_ltac_tactics.ml4 | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 102918e5e5..a91ff98fb9 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -401,11 +401,11 @@ let print_results ~cutoff = print_results_filter ~cutoff ~filter:(fun _ -> true) let print_results_tactic tactic = - print_results_filter ~cutoff:0.0 ~filter:(fun s -> + print_results_filter ~cutoff:!Flags.profile_ltac_cutoff ~filter:(fun s -> String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic))))) let do_print_results_at_close () = - if get_profiling () then print_results ~cutoff:0.0 + if get_profiling () then print_results ~cutoff:!Flags.profile_ltac_cutoff let _ = Declaremods.append_end_library_hook do_print_results_at_close diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index 9083bda60a..8cb76d81c5 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -31,7 +31,7 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY -| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ] +| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ] | [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] END |