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

feat(frontends/lean/parser): recognize padded Exprs terminators

Browse source
This commit is contained in:
Sebastian Ullrich 2015-10-09 18:17:06 +02:00 committed by Leonardo de Moura
parent dbfebd5409
commit 7c047def97
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/parser.cpp
View file

@ -1181,7 +1181,7 @@ static bool curr_is_terminator_of_exprs_action(parser const & p, list<pair<notat
notation::action const & a = pr.first.get_action();
if (a.kind() == notation::action_kind::Exprs &&
a.get_terminator() &&
p.curr_is_token(*a.get_terminator())) {
p.curr_is_token(name(utf8_trim(a.get_terminator()->to_string())))) {
r = &pr;
return true;
}
@ -1265,9 +1265,11 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) {
case notation::action_kind::Exprs: {
buffer<expr> r_args;
auto terminator = a.get_terminator();
if (terminator)
terminator = some(name(utf8_trim(terminator->to_string()))); // remove padding
if (!terminator || !curr_is_token(*terminator)) {
r_args.push_back(parse_expr_or_tactic(a.rbp(), as_tactic));
name sep = utf8_trim(a.get_sep().to_string());
name sep = utf8_trim(a.get_sep().to_string()); // remove padding
while (curr_is_token(sep)) {
next();
r_args.push_back(parse_expr_or_tactic(a.rbp(), as_tactic));