From 7c047def97a655df64ee4a6300b3f68b1a1fd47d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 9 Oct 2015 18:17:06 +0200
Subject: [PATCH] feat(frontends/lean/parser): recognize padded Exprs
 terminators

---
 src/frontends/lean/parser.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 218473d73..f3bab8199 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -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));