From fa26c2301cdfd14c83f85242646e2b5d63f36b8d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Nov 2014 14:49:43 -0800 Subject: [PATCH] fix(frontends/lean): fix pretty-printing spacing problem --- src/frontends/lean/pp.cpp | 9 ++++++++- tests/lean/tactic_var_bug.lean.expected.out | 2 -- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 286458718..c40a53438 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -741,6 +741,13 @@ auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> } } +static bool add_extra_space_first(name const & tk) { + // TODO(Leo): this is a hard-coded temporary solution for deciding whether extra + // spaces should be added or not when pretty printing notation. + // We should implement a better solution in the future. + return tk != "(" && tk != ")"; +} + static bool add_extra_space(name const & tk) { // TODO(Leo): this is a hard-coded temporary solution for deciding whether extra // spaces should be added or not when pretty printing notation. @@ -852,7 +859,7 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer> --i; result arg_res = pp_notation_child(rec_args[i], curr_lbp, a.rbp()); if (i == 0) { - if (add_extra_space(tk)) + if (add_extra_space_first(tk)) curr = format(tk) + space() + arg_res.fmt() + curr; else curr = format(tk) + arg_res.fmt() + curr; diff --git a/tests/lean/tactic_var_bug.lean.expected.out b/tests/lean/tactic_var_bug.lean.expected.out index 620d7160e..e69de29bb 100644 --- a/tests/lean/tactic_var_bug.lean.expected.out +++ b/tests/lean/tactic_var_bug.lean.expected.out @@ -1,2 +0,0 @@ -type: Pi (q : notation_info (no_info Prop)) (a : q), true -value: fun (q : notation_info (no_info Prop)), (by (begin_end (tactic.and_then (begin_end_element (tactic.intro r)) (begin_end_element (tactic.apply true.intro)))))