michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/pp): avoid unnecessary parentheses when pretty printing delimited notation

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-23 14:14:08 -07:00
parent 43cfd5c26a
commit 20ab59c740
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/pp.cpp
View file

@ -737,7 +737,7 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
case notation::action_kind::Skip: case notation::action_kind::Skip:
curr = format(tk); curr = format(tk);
if (last) if (last)
last_rbp = get_some_precedence(m_token_table, tk); last_rbp = max_bp();
break; break;
case notation::action_kind::Expr: case notation::action_kind::Expr:
if (args.empty() || !args.back()) { if (args.empty() || !args.back()) {
@ -873,8 +873,9 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
} }
extra_space = add_extra_space(tk); extra_space = add_extra_space(tk);
} }
unsigned first_lbp = token_lbp; unsigned first_lbp = max_bp();
if (!entry.is_nud()) { if (!entry.is_nud()) {
first_lbp = token_lbp;
lean_assert(!last); lean_assert(!last);
if (args.size() != 1 || !args.back()) if (args.size() != 1 || !args.back())
return optional<result>(); return optional<result>();