From 17204f9629cdcf55972dd13b8d46f4a4396ff09e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 11 Apr 2017 13:31:48 +0200 Subject: [PATCH] feat(library/vm/interaction_state): capture tactic profile data if enabled --- src/library/vm/interaction_state.h | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/library/vm/interaction_state.h b/src/library/vm/interaction_state.h index 2a5672f632..902a497bf0 100644 --- a/src/library/vm/interaction_state.h +++ b/src/library/vm/interaction_state.h @@ -26,6 +26,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich #include "library/scoped_ext.h" #include "library/aux_definition.h" #include "library/unfold_macros.h" +#include "library/message_builder.h" #include "library/vm/vm.h" #include "library/vm/vm_environment.h" #include "library/vm/vm_exceptional.h" @@ -235,7 +236,17 @@ struct interaction_monad { name interaction_name("_interaction"); environment new_env = compile(interaction_name, interaction); vm_state S(new_env, m_opts); + vm_state::profiler prof(S, m_opts); vm_obj r = invoke(S, interaction_name, {to_obj(s)}); + if (prof.enabled()) { + auto out = message_builder(environment(), get_global_ios(), + get_pos_info_provider()->get_file_name(), + get_pos_info_provider()->get_pos_info_or_some(interaction), + INFORMATION); + out.set_caption("tactic profile data"); + prof.get_snapshots().display(out.get_text_stream().get_stream()); + out.report(); + } if (!is_success(r)) process_failure(S, r);