From d03dc18096f519c874c14a523501ca7ec17bc02c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Jun 2016 10:47:48 -0700 Subject: [PATCH] chore(library/tactic/tactic_state): add helper methods --- src/library/tactic/tactic_state.cpp | 16 ++++++++++++---- src/library/tactic/tactic_state.h | 2 ++ 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 30bc19295c..ab2bd21681 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -114,6 +114,16 @@ format tactic_state::pp(formatter_factory const & fmtf) const { return r; } +format tactic_state::pp() const { + formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); + return pp(fmtf); +} + +format tactic_state::pp_expr(expr const & e) const { + formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); + return pp_expr(fmtf, e); +} + struct vm_tactic_state : public vm_external { tactic_state m_val; vm_tactic_state(tactic_state const & v):m_val(v) {} @@ -146,13 +156,11 @@ vm_obj tactic_state_env(vm_obj const & s) { } vm_obj tactic_state_to_format(vm_obj const & s) { - formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); - return to_obj(to_tactic_state(s).pp(fmtf)); + return to_obj(to_tactic_state(s).pp()); } format pp_expr(tactic_state const & s, expr const & e) { - formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); - return s.pp_expr(fmtf, e); + return s.pp_expr(e); } format pp_indented_expr(tactic_state const & s, expr const & e) { diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index 0cd9e6ef47..cfe34ecc0a 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -60,6 +60,8 @@ public: format pp(formatter_factory const & fmtf) const; format pp_expr(formatter_factory const & fmtf, expr const & e) const; + format pp() const; + format pp_expr(expr const & e) const; }; inline bool operator==(tactic_state const & s1, tactic_state const & s2) { return is_eqp(s1, s2); }