From fd40999909ac7202f03c4fe43289f3191b6f124a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Oct 2014 15:52:06 -0700 Subject: [PATCH] feat(frontends/lean): uniform unsolved goals "error" position --- src/frontends/lean/builtin_exprs.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index a03eb9c72..93aba87ac 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -154,6 +154,11 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) { tacs.push_back(tac); } expr r = tacs[0]; + if (tacs.size() == 1) { + // Hack: for having a uniform squiggle placement for unsolved goals. + // That is, the result is always of the form and_then(...). + r = p.mk_app({get_and_then_tac_fn(), r, get_id_tac_fn()}, end_pos); + } for (unsigned i = 1; i < tacs.size(); i++) { r = p.mk_app({get_and_then_tac_fn(), r, tacs[i]}, end_pos); }