Merge pull request #270 from eric-wieser/add-binder-highlighting

fix(syntaxes/lean): implicit binder brackets are forbidden in symbol names
leanprover · May 26, 2021 · 346bb62 · 346bb62
2 parents bfa80de + 6b973c1
commit 346bb62
Showing 1 changed file with 4 additions and 3 deletions.
diff --git 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" : [