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

fix(frontends/lean): fix pretty-printing spacing problem

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-09 14:49:43 -08:00
parent 3aac26d658
commit fa26c2301c
2 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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<optional<expr>>
--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;

2
tests/lean/tactic_var_bug.lean.expected.out
View file

@ -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)))))