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

fix(frontends/lean/pp): extra space

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-31 15:07:32 -07:00
parent 26c914173c
commit 4eb270a572
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1040,7 +1040,8 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
curr = curr + space(); curr = curr + space();
fmt = curr + fmt; fmt = curr + fmt;
} }
extra_space = add_extra_space(tk); if (m_extra_spaces || !last_is_skip)
extra_space = add_extra_space(tk);
} }
unsigned first_lbp = inf_bp(); unsigned first_lbp = inf_bp();
if (!entry.is_nud()) { if (!entry.is_nud()) {