From 3fa1829b225bb9e9ed2bca0eedaf4b83f0c403e1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 27 Jun 2015 14:00:09 -0700 Subject: [PATCH] feat(frontends/lean/migrate_cmd): add profile for migrate command --- src/frontends/lean/migrate_cmd.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/migrate_cmd.cpp b/src/frontends/lean/migrate_cmd.cpp index e8b148eab..c76945ae1 100644 --- a/src/frontends/lean/migrate_cmd.cpp +++ b/src/frontends/lean/migrate_cmd.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/timeit.h" #include "util/sexpr/option_declarations.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" @@ -440,7 +441,16 @@ struct migrate_cmd_fn { }; static environment migrate_cmd(parser & p) { - return migrate_cmd_fn(p)(); + if (p.profiling()) { + auto pos = p.pos(); + std::ostringstream msg; + ::lean::display_pos(msg, p.get_stream_name().c_str(), pos.first, pos.second); + msg << " migrate cmd time"; + timeit timer(p.diagnostic_stream().get_stream(), msg.str().c_str()); + return migrate_cmd_fn(p)(); + } else { + return migrate_cmd_fn(p)(); + } } void register_migrate_cmd(cmd_table & r) {