blob: 0c4e0b075780bdfebe762d077e6a93b5c5d9a466 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
(*i camlp4deps: "grammar/grammar.cma" i*)
open Profile_ltac
open Stdarg
DECLARE PLUGIN "profile_ltac_plugin"
let tclSET_PROFILING b =
Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
set_profiling b))
TACTIC EXTEND start_profiling
| [ "start" "profiling" ] -> [ tclSET_PROFILING true ]
END
TACTIC EXTEND stop_profiling
| [ "stop" "profiling" ] -> [ tclSET_PROFILING false ]
END;;
VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF
[ "Start" "Profiling" ] -> [ reset_profile(); set_profiling true ]
END
VERNAC COMMAND EXTEND StopProfiling CLASSIFIED AS SIDEFF
[ "Stop" "Profiling" ] -> [ set_profiling false ]
END
VERNAC COMMAND EXTEND ResetProfiling CLASSIFIED AS SIDEFF
[ "Reset" "Profile" ] -> [ reset_profile() ]
END
VERNAC COMMAND EXTEND ShowProfile CLASSIFIED AS QUERY
[ "Show" "Profile" ] -> [ print_results() ]
END
VERNAC COMMAND EXTEND ShowProfileTactic CLASSIFIED AS QUERY
[ "Show" "Profile" string(s) ] -> [ print_results_tactic s ]
END
|
