From 49b2bb209dd07295ca3adf20923f2f0c05d6502d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 May 2014 13:11:54 -0700 Subject: [PATCH] refactor(kernel/formatter): formatter_cell object should not perform destructive updates Signed-off-by: Leonardo de Moura --- src/kernel/formatter.cpp | 2 +- src/kernel/formatter.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index 6cbe06927a..f911d7bd78 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -213,7 +213,7 @@ std::ostream & operator<<(std::ostream & out, expr const & e) { class simple_formatter_cell : public formatter_cell { public: - virtual format operator()(environment const & env, expr const & e, options const &) { + virtual format operator()(environment const & env, expr const & e, options const &) const { std::ostringstream s; print_expr_fn pr(s, env.prop_proof_irrel()); pr(e); diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index da5b048e68..38cdd79cee 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -30,7 +30,7 @@ class formatter_cell { public: virtual ~formatter_cell() {} /** \brief Format the given expression. */ - virtual format operator()(environment const & env, expr const & e, options const & opts) = 0; + virtual format operator()(environment const & env, expr const & e, options const & opts) const = 0; }; /** \brief Smart-pointer for the actual formatter object (aka \c formatter_cell).