From 7a0158dcabebf868f8762043e077ebef08249237 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Aug 2016 15:47:49 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): must take (updated) configuration options into account --- src/frontends/lean/elaborator.cpp | 4 ++++ src/frontends/lean/elaborator.h | 1 + 2 files changed, 5 insertions(+) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 675ac3b37b..730b7e35d2 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -63,6 +63,10 @@ elaborator::elaborator(environment const & env, options const & opts, metavar_co m_ctx(mctx, lctx, get_elab_tc_cache_for(env, opts), transparency_mode::Semireducible) { } +auto elaborator::mk_pp_ctx(type_context const & ctx) -> pp_fn { + return ::lean::mk_pp_ctx(ctx.env(), m_opts, ctx.mctx(), ctx.lctx()); +} + format elaborator::pp_indent(pp_fn const & pp_fn, expr const & e) { unsigned i = get_pp_indent(m_opts); return nest(i, line() + pp_fn(e)); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 67e5350001..8ee268262a 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -83,6 +83,7 @@ private: expr get_default_numeral_type(); typedef std::function pp_fn; + pp_fn mk_pp_ctx(type_context const & ctx); format pp_indent(pp_fn const & pp_fn, expr const & e); format pp_indent(expr const & e); format pp_overloads(pp_fn const & pp_fn, buffer const & fns);