From 34b227ed0916e984eb4410c468f217dd1a79a84b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 26 May 2021 15:51:44 +0100
Subject: [PATCH 1/2] fix(syntaxes/lean): implicit binder brackets are
 forbidden in symbol names

---
 syntaxes/lean.json | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/syntaxes/lean.json b/syntaxes/lean.json
index 6b6d520..d287c79 100644
--- a/syntaxes/lean.json
+++ b/syntaxes/lean.json
@@ -164,6 +164,7 @@
           "name": "meta.parens",
           "patterns" : [
             { "begin": ":", "end": "(?=\\))",
+              "beginCaptures": {"0": {"name": "punctuation.separator.type.lean"}},
               "contentName": "meta.type.lean",
               "patterns" : [
                 {"include": "#expressions"}
@@ -224,13 +225,13 @@
     },
     "definitionName": {
       "patterns": [
-        {"match": "\\b[^:«»\\(\\)\\{\\},[:space:]=→λ∀?][^:«»\\(\\)\\{\\},[:space:]]*", "name": "entity.name.function.lean"},
+        {"match": "\\b[^:«»\\(\\)\\{\\}⦃⦄,[:space:]=→λ∀?][^:«»\\(\\)\\{\\}⦃⦄,[:space:]]*", "name": "entity.name.function.lean"},
         {"begin": "«", "end": "»", "contentName": "entity.name.function.lean"}
       ]
     },
     "binderName": {
       "patterns": [
-        {"match": "\\b[^:«»\\(\\)\\{\\},[:space:]=→λ∀?][^:«»\\(\\)\\{\\},[:space:]]*", "name": "variable.parameter.lean"},
+        {"match": "\\b[^:«»\\(\\)\\{\\}⦃⦄,[:space:]=→λ∀?][^:«»\\(\\)\\{\\}⦃⦄,[:space:]]*", "name": "variable.parameter.lean"},
         {"begin": "«", "end": "»", "contentName": "variable.parameter.lean"}
       ]
     },
@@ -275,7 +276,7 @@
           "beginCaptures": {"0": {"name": "punctuation.definition.binder.semiimplicit.begin.lean"}},
           "endCaptures": {"0": {"name": "punctuation.definition.binder.semiimplicit.end.lean"}},
           "patterns" : [
-            { "begin": ":", "end": "(?=\\⦄)",
+            { "begin": ":", "end": "(?=⦄|\\})",
               "beginCaptures": {"0": {"name": "punctuation.separator.type.lean"}},
               "contentName": "meta.type.lean",
               "patterns" : [

From 6b973c1d5673211bf27b0cd2316400d943543164 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 26 May 2021 15:55:37 +0100
Subject: [PATCH 2/2] Update syntaxes/lean.json

---
 syntaxes/lean.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/syntaxes/lean.json b/syntaxes/lean.json
index d287c79..67124a6 100644
--- a/syntaxes/lean.json
+++ b/syntaxes/lean.json
@@ -276,7 +276,7 @@
           "beginCaptures": {"0": {"name": "punctuation.definition.binder.semiimplicit.begin.lean"}},
           "endCaptures": {"0": {"name": "punctuation.definition.binder.semiimplicit.end.lean"}},
           "patterns" : [
-            { "begin": ":", "end": "(?=⦄|\\})",
+            { "begin": ":", "end": "(?=⦄|\\}\\})",
               "beginCaptures": {"0": {"name": "punctuation.separator.type.lean"}},
               "contentName": "meta.type.lean",
               "patterns" : [