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

Fix bug in pretty printer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-18 10:45:12 -07:00
parent 18f319d00f
commit 7ec7b4dce8
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontend/pp.cpp
View file

@ -304,6 +304,7 @@ class pp_fn {
for (unsigned i = 1; i < num_args(e); i++) { for (unsigned i = 1; i < num_args(e); i++) {
result p_arg = pp_mixfix_child(op, arg(e, i), depth); result p_arg = pp_mixfix_child(op, arg(e, i), depth);
unsigned sz = it->size(); unsigned sz = it->size();
if (i > 1) r_format += space();
r_format += format{format(*it), nest(sz+1, format{line(), p_arg.first})}; r_format += format{format(*it), nest(sz+1, format{line(), p_arg.first})};
r_depth = std::max(r_depth, p_arg.second); r_depth = std::max(r_depth, p_arg.second);
++it; ++it;