equal
deleted
inserted
replaced
82 is_relevant_time elapsed orelse |
82 is_relevant_time elapsed orelse |
83 is_relevant_time cpu orelse |
83 is_relevant_time cpu orelse |
84 is_relevant_time gc; |
84 is_relevant_time gc; |
85 |
85 |
86 fun message {elapsed, cpu, gc} = |
86 fun message {elapsed, cpu, gc} = |
87 Time.toString elapsed ^ "s elapsed time, " ^ |
87 Value.print_time elapsed ^ "s elapsed time, " ^ |
88 Time.toString cpu ^ "s cpu time, " ^ |
88 Value.print_time cpu ^ "s cpu time, " ^ |
89 Time.toString gc ^ "s GC time" handle Time.Time => ""; |
89 Value.print_time gc ^ "s GC time" handle Time.Time => ""; |
90 |
90 |
91 fun cond_timeit enabled msg e = |
91 fun cond_timeit enabled msg e = |
92 if enabled then |
92 if enabled then |
93 let |
93 let |
94 val (t, result) = timing (Exn.interruptible_capture e) (); |
94 val (t, result) = timing (Exn.interruptible_capture e) (); |