source.lean.json in github-linguist-7.12.0

- old
+ new
@@ -1,226 +2 @@
-{
-  "name": "Lean",
-  "scopeName": "source.lean",
-  "patterns": [
-    {
-      "include": "#comments"
-    },
-    {
-      "name": "meta.definitioncommand.lean",
-      "begin": "\\b(?\u003c!\\.)(inductive|coinductive|structure|theorem|axiom|axioms|abbreviation|lemma|definition|def|instance|class|constant)\\b\\s+(\\{[^}]*\\})?",
-      "end": "(?=\\bwith\\b|\\bextends\\b|[:\\|\\(\\[\\{⦃\u003c\u003e])",
-      "patterns": [
-        {
-          "include": "#comments"
-        },
-        {
-          "include": "#definitionName"
-        },
-        {
-          "match": ","
-        }
-      ],
-      "beginCaptures": {
-        "1": {
-          "name": "keyword.other.definitioncommand.lean"
-        }
-      }
-    },
-    {
-      "name": "storage.type.lean",
-      "match": "\\b(Prop|Type|Sort)\\b"
-    },
-    {
-      "name": "storage.modifier.lean",
-      "match": "\\battribute\\b\\s*\\[[^\\]]*\\]"
-    },
-    {
-      "name": "storage.modifier.lean",
-      "match": "@\\[[^\\]]*\\]"
-    },
-    {
-      "name": "keyword.control.definition.modifier.lean",
-      "match": "\\b(?\u003c!\\.)(private|meta|mutual|protected|noncomputable)\\b"
-    },
-    {
-      "name": "invalid.illegal.lean",
-      "match": "\\b(sorry)\\b"
-    },
-    {
-      "name": "keyword.other.command.lean",
-      "match": "#print\\s+(def|definition|inductive|instance|structure|axiom|axioms|class)\\b"
-    },
-    {
-      "name": "keyword.other.command.lean",
-      "match": "#(print|eval|reduce|check|help|exit|find|where)\\b"
-    },
-    {
-      "name": "keyword.other.lean",
-      "match": "\\b(?\u003c!\\.)(import|export|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd|restate_axiom)(?!\\.)\\b"
-    },
-    {
-      "name": "keyword.other.lean",
-      "match": "\\b(?\u003c!\\.)(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from|obtain|haveI|λ)(?!\\.)\\b"
-    },
-    {
-      "contentName": "entity.name.lean",
-      "begin": "«",
-      "end": "»"
-    },
-    {
-      "name": "keyword.control.lean",
-      "match": "\\b(?\u003c!\\.)(if|then|else)\\b"
-    },
-    {
-      "name": "string.quoted.double.lean",
-      "begin": "\"",
-      "end": "\"",
-      "patterns": [
-        {
-          "name": "constant.character.escape.lean",
-          "match": "\\\\[\\\\\"nt']"
-        },
-        {
-          "name": "constant.character.escape.lean",
-          "match": "\\\\x[0-9A-Fa-f][0-9A-Fa-f]"
-        },
-        {
-          "name": "constant.character.escape.lean",
-          "match": "\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]"
-        }
-      ],
-      "beginCaptures": {
-        "0": {
-          "name": "punctuation.definition.string.begin.lean"
-        }
-      },
-      "endCaptures": {
-        "0": {
-          "name": "punctuation.definition.string.end.lean"
-        }
-      }
-    },
-    {
-      "name": "string.quoted.single.lean",
-      "match": "'[^\\\\']'"
-    },
-    {
-      "name": "string.quoted.single.lean",
-      "match": "'(\\\\(x..|u....|.))'",
-      "captures": {
-        "1": {
-          "name": "constant.character.escape.lean"
-        }
-      }
-    },
-    {
-      "name": "entity.name.lean",
-      "match": "`+[^\\[(]\\S+"
-    },
-    {
-      "name": "constant.numeric.lean",
-      "match": "\\b([0-9]+|0([xX][0-9a-fA-F]+))\\b"
-    }
-  ],
-  "repository": {
-    "blockComment": {
-      "name": "comment.block.lean",
-      "begin": "/-",
-      "end": "-/",
-      "patterns": [
-        {
-          "include": "source.lean.markdown"
-        },
-        {
-          "include": "#blockComment"
-        }
-      ]
-    },
-    "comments": {
-      "patterns": [
-        {
-          "include": "#dashComment"
-        },
-        {
-          "include": "#docComment"
-        },
-        {
-          "include": "#stringBlock"
-        },
-        {
-          "include": "#modDocComment"
-        },
-        {
-          "include": "#blockComment"
-        }
-      ]
-    },
-    "dashComment": {
-      "name": "comment.line.double-dash.lean",
-      "begin": "(--)",
-      "end": "$",
-      "patterns": [
-        {
-          "include": "source.lean.markdown"
-        }
-      ],
-      "beginCaptures": {
-        "0": {
-          "name": "punctuation.definition.comment.lean"
-        }
-      }
-    },
-    "definitionName": {
-      "patterns": [
-        {
-          "name": "entity.name.function.lean",
-          "match": "\\b[^:«»\\(\\)\\{\\}[:space:]=→λ∀?][^:«»\\(\\)\\{\\}[:space:]]*"
-        },
-        {
-          "contentName": "entity.name.function.lean",
-          "begin": "«",
-          "end": "»"
-        }
-      ]
-    },
-    "docComment": {
-      "name": "comment.block.documentation.lean",
-      "begin": "/--",
-      "end": "-/",
-      "patterns": [
-        {
-          "include": "source.lean.markdown"
-        },
-        {
-          "include": "#blockComment"
-        }
-      ]
-    },
-    "modDocComment": {
-      "name": "comment.block.documentation.lean",
-      "begin": "/-!",
-      "end": "-/",
-      "patterns": [
-        {
-          "include": "source.lean.markdown"
-        },
-        {
-          "include": "#blockComment"
-        }
-      ]
-    },
-    "stringBlock": {
-      "name": "comment.block.string.lean",
-      "begin": "/-\"",
-      "end": "\"-/",
-      "patterns": [
-        {
-          "include": "source.lean.markdown"
-        },
-        {
-          "include": "#blockComment"
-        }
-      ]
-    }
-  }
-}
+{"name":"Lean","scopeName":"source.lean","patterns":[{"include":"#comments"},{"name":"meta.definitioncommand.lean","begin":"\\b(?\u003c!\\.)(inductive|coinductive|structure|theorem|axiom|axioms|abbreviation|lemma|definition|def|instance|class|constant)\\b\\s+(\\{[^}]*\\})?","end":"(?=\\bwith\\b|\\bextends\\b|[:\\|\\(\\[\\{⦃\u003c\u003e])","patterns":[{"include":"#comments"},{"include":"#definitionName"},{"match":","}],"beginCaptures":{"1":{"name":"keyword.other.definitioncommand.lean"}}},{"name":"storage.type.lean","match":"\\b(Prop|Type|Sort)\\b"},{"name":"storage.modifier.lean","match":"\\battribute\\b\\s*\\[[^\\]]*\\]"},{"name":"storage.modifier.lean","match":"@\\[[^\\]]*\\]"},{"name":"keyword.control.definition.modifier.lean","match":"\\b(?\u003c!\\.)(private|meta|mutual|protected|noncomputable)\\b"},{"name":"invalid.illegal.lean","match":"\\b(sorry)\\b"},{"name":"keyword.other.command.lean","match":"#print\\s+(def|definition|inductive|instance|structure|axiom|axioms|class)\\b"},{"name":"keyword.other.command.lean","match":"#(print|eval|reduce|check|help|exit|find|where)\\b"},{"name":"keyword.other.lean","match":"\\b(?\u003c!\\.)(import|export|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd|restate_axiom)(?!\\.)\\b"},{"name":"keyword.other.lean","match":"\\b(?\u003c!\\.)(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from|obtain|haveI|λ)(?!\\.)\\b"},{"contentName":"entity.name.lean","begin":"«","end":"»"},{"name":"keyword.control.lean","match":"\\b(?\u003c!\\.)(if|then|else)\\b"},{"name":"string.quoted.double.lean","begin":"\"","end":"\"","patterns":[{"name":"constant.character.escape.lean","match":"\\\\[\\\\\"nt']"},{"name":"constant.character.escape.lean","match":"\\\\x[0-9A-Fa-f][0-9A-Fa-f]"},{"name":"constant.character.escape.lean","match":"\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]"}],"beginCaptures":{"0":{"name":"punctuation.definition.string.begin.lean"}},"endCaptures":{"0":{"name":"punctuation.definition.string.end.lean"}}},{"name":"string.quoted.single.lean","match":"'[^\\\\']'"},{"name":"string.quoted.single.lean","match":"'(\\\\(x..|u....|.))'","captures":{"1":{"name":"constant.character.escape.lean"}}},{"name":"entity.name.lean","match":"`+[^\\[(]\\S+"},{"name":"constant.numeric.lean","match":"\\b([0-9]+|0([xX][0-9a-fA-F]+))\\b"}],"repository":{"blockComment":{"name":"comment.block.lean","begin":"/-","end":"-/","patterns":[{"include":"source.lean.markdown"},{"include":"#blockComment"}]},"comments":{"patterns":[{"include":"#dashComment"},{"include":"#docComment"},{"include":"#stringBlock"},{"include":"#modDocComment"},{"include":"#blockComment"}]},"dashComment":{"name":"comment.line.double-dash.lean","begin":"(--)","end":"$","patterns":[{"include":"source.lean.markdown"}],"beginCaptures":{"0":{"name":"punctuation.definition.comment.lean"}}},"definitionName":{"patterns":[{"name":"entity.name.function.lean","match":"\\b[^:«»\\(\\)\\{\\}[:space:]=→λ∀?][^:«»\\(\\)\\{\\}[:space:]]*"},{"contentName":"entity.name.function.lean","begin":"«","end":"»"}]},"docComment":{"name":"comment.block.documentation.lean","begin":"/--","end":"-/","patterns":[{"include":"source.lean.markdown"},{"include":"#blockComment"}]},"modDocComment":{"name":"comment.block.documentation.lean","begin":"/-!","end":"-/","patterns":[{"include":"source.lean.markdown"},{"include":"#blockComment"}]},"stringBlock":{"name":"comment.block.string.lean","begin":"/-\"","end":"\"-/","patterns":[{"include":"source.lean.markdown"},{"include":"#blockComment"}]}}}