From 80ec48c93d07201f4d64fe2c7a7bb1b75feb8d18 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Aug 2013 12:33:19 -0700 Subject: [PATCH] Make sure formatter can be used even when associated frontend is not in scope. Signed-off-by: Leonardo de Moura --- src/frontend/pp.cpp | 6 +++--- src/tests/frontend/frontend.cpp | 13 ++++++++++++- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/frontend/pp.cpp b/src/frontend/pp.cpp index 6114f1cd3..0b0dfeb00 100644 --- a/src/frontend/pp.cpp +++ b/src/frontend/pp.cpp @@ -574,9 +574,9 @@ public: }; class pp_formatter_cell : public formatter_cell { - frontend const & m_frontend; - options m_options; - unsigned m_indent; + frontend m_frontend; + options m_options; + unsigned m_indent; format pp(expr const & e) { return pp_fn(m_frontend, m_options)(e); diff --git a/src/tests/frontend/frontend.cpp b/src/tests/frontend/frontend.cpp index e4a6392c1..4638e3b44 100644 --- a/src/tests/frontend/frontend.cpp +++ b/src/tests/frontend/frontend.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "environment.h" #include "operator_info.h" #include "kernel_exception.h" +#include "builtin.h" #include "pp.h" #include "test.h" using namespace lean; @@ -57,7 +58,6 @@ static void tst3() { static void tst4() { frontend f; formatter fmt = mk_pp_formatter(f); - expr Bool = Const("Bool"); context c; c = extend(c, "x", Bool); c = extend(c, "y", Bool); @@ -105,6 +105,16 @@ static void tst6() { std::cout << fmt(env) << "\n"; } +static formatter mk() { + frontend f; + return mk_pp_formatter(f); +} + +static void tst7() { + formatter fmt = mk(); + std::cout << fmt(And(Const("x"), Const("y"))) << "\n"; +} + int main() { tst1(); tst2(); @@ -112,5 +122,6 @@ int main() { tst4(); tst5(); tst6(); + tst7(); return has_violations() ? 1 : 0; }