source.lean4.json in github-linguist-7.29.0

- old
+ new
@@ -1 +1 @@
-{"name":"Lean 4","scopeName":"source.lean4","patterns":[{"include":"#comments"},{"name":"storage.type.lean4","match":"\\b(Prop|Type|Sort)\\b"},{"name":"storage.modifier.lean4","match":"\\battribute\\b\\s*\\[[^\\]]*\\]"},{"name":"storage.modifier.lean4","match":"@\\[[^\\]]*\\]"},{"name":"storage.modifier.lean4","match":"\\b(?\u003c!\\.)(global|local|scoped|partial|unsafe|private|protected|noncomputable)(?!\\.)\\b"},{"name":"invalid.illegal.lean4","match":"\\bsorry\\b"},{"name":"keyword.other.lean4","match":"#(print|eval|reduce|check|check_failure)\\b"},{"name":"keyword.other.command.lean4","match":"\\bderiving\\s+instance\\b"},{"name":"meta.definitioncommand.lean4","begin":"\\b(?\u003c!\\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\\b\\s+(\\{[^}]*\\})?","end":"(?=\\bwith\\b|\\bextends\\b|\\bwhere\\b|[:\\|\\(\\[\\{⦃\u003c\u003e])","patterns":[{"include":"#comments"},{"include":"#definitionName"},{"match":","}],"beginCaptures":{"1":{"name":"keyword.other.definitioncommand.lean4"}}},{"name":"keyword.other.lean4","match":"\\b(?\u003c!\\.)(theorem|show|have|from|suffices|nomatch|def|class|structure|instance|set_option|initialize|builtin_initialize|example|inductive|coinductive|axiom|constant|universe|universes|variable|variables|import|open|export|theory|prelude|renaming|hiding|exposing|do|by|let|extends|mutual|mut|where|rec|syntax|macro_rules|macro|deriving|fun|section|namespace|end|infix|infixl|infixr|postfix|prefix|notation|abbrev|if|then|else|calc|match|with|for|in|unless|try|catch|finally|return|continue|break)(?!\\.)\\b"},{"contentName":"entity.name.lean4","begin":"«","end":"»"},{"name":"string.quoted.double.lean4","begin":"\"","end":"\"","patterns":[{"name":"constant.character.escape.lean4","match":"\\\\[\\\\\"ntr']"},{"name":"constant.character.escape.lean4","match":"\\\\x[0-9A-Fa-f][0-9A-Fa-f]"},{"name":"constant.character.escape.lean4","match":"\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]"}]},{"name":"constant.language.lean4","match":"\\b(true|false)\\b"},{"name":"string.quoted.single.lean4","match":"'[^\\\\']'"},{"name":"string.quoted.single.lean4","match":"'(\\\\(x[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'","captures":{"1":{"name":"constant.character.escape.lean4"}}},{"name":"entity.name.lean4","match":"`+[^\\[(]\\S+"},{"name":"constant.numeric.lean4","match":"\\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(0|[1-9][0-9]*)(\\.[0-9]+)?([eE][+-]?[0-9]+)?)\\b"}],"repository":{"blockComment":{"name":"comment.block.lean4","begin":"/-","end":"-/","patterns":[{"include":"source.lean4.markdown"},{"include":"#blockComment"}]},"comments":{"patterns":[{"include":"#dashComment"},{"include":"#docComment"},{"include":"#stringBlock"},{"include":"#modDocComment"},{"include":"#blockComment"}]},"dashComment":{"name":"comment.line.double-dash.lean4","begin":"--","end":"$","patterns":[{"include":"source.lean4.markdown"}]},"definitionName":{"patterns":[{"name":"entity.name.function.lean4","match":"\\b[^:«»\\(\\)\\{\\}[:space:]=→λ∀?][^:«»\\(\\)\\{\\}[:space:]]*"},{"contentName":"entity.name.function.lean4","begin":"«","end":"»"}]},"docComment":{"name":"comment.block.documentation.lean4","begin":"/--","end":"-/","patterns":[{"include":"source.lean4.markdown"},{"include":"#blockComment"}]},"modDocComment":{"name":"comment.block.documentation.lean4","begin":"/-!","end":"-/","patterns":[{"include":"source.lean4.markdown"},{"include":"#blockComment"}]}}}
+{"name":"Lean 4","scopeName":"source.lean4","patterns":[{"include":"#comments"},{"name":"storage.type.lean4","match":"\\b(Prop|Type|Sort)\\b"},{"name":"storage.modifier.lean4","match":"\\battribute\\b\\s*\\[[^\\]]*\\]"},{"name":"storage.modifier.lean4","match":"@\\[[^\\]]*\\]"},{"name":"storage.modifier.lean4","match":"\\b(?\u003c!\\.)(global|local|scoped|partial|unsafe|private|protected|noncomputable)(?!\\.)\\b"},{"name":"invalid.illegal.lean4","match":"\\b(sorry|admit|stop)\\b"},{"name":"keyword.other.lean4","match":"#(print|eval|reduce|check|check_failure)\\b"},{"name":"keyword.other.command.lean4","match":"\\bderiving\\s+instance\\b"},{"name":"meta.definitioncommand.lean4","begin":"\\b(?\u003c!\\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\\b\\s+(\\{[^}]*\\})?","end":"(?=\\bwith\\b|\\bextends\\b|\\bwhere\\b|[:\\|\\(\\[\\{⦃\u003c\u003e])","patterns":[{"include":"#comments"},{"include":"#definitionName"},{"match":","}],"beginCaptures":{"1":{"name":"keyword.other.definitioncommand.lean4"}}},{"name":"keyword.other.lean4","match":"\\b(?\u003c!\\.)(theorem|show|have|from|suffices|nomatch|def|class|structure|instance|set_option|initialize|builtin_initialize|example|inductive|coinductive|axiom|constant|universe|universes|variable|variables|import|open|export|theory|prelude|renaming|hiding|exposing|do|by|let|extends|mutual|mut|where|rec|syntax|macro_rules|macro|deriving|fun|section|namespace|end|infix|infixl|infixr|postfix|prefix|notation|abbrev|if|then|else|calc|match|with|for|in|unless|try|catch|finally|return|continue|break)(?!\\.)\\b"},{"contentName":"entity.name.lean4","begin":"«","end":"»"},{"name":"string.interpolated.lean4","begin":"(s!)\"","end":"\"","patterns":[{"begin":"(\\{)","end":"(\\})","patterns":[{"include":"$self"}],"beginCaptures":{"1":{"name":"keyword.other.lean4"}},"endCaptures":{"1":{"name":"keyword.other.lean4"}}},{"name":"constant.character.escape.lean4","match":"\\\\[\\\\\"ntr']"},{"name":"constant.character.escape.lean4","match":"\\\\x[0-9A-Fa-f][0-9A-Fa-f]"},{"name":"constant.character.escape.lean4","match":"\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]"}],"beginCaptures":{"1":{"name":"keyword.other.lean4"}}},{"name":"string.quoted.double.lean4","begin":"\"","end":"\"","patterns":[{"name":"constant.character.escape.lean4","match":"\\\\[\\\\\"ntr']"},{"name":"constant.character.escape.lean4","match":"\\\\x[0-9A-Fa-f][0-9A-Fa-f]"},{"name":"constant.character.escape.lean4","match":"\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]"}]},{"name":"constant.language.lean4","match":"\\b(true|false)\\b"},{"name":"string.quoted.single.lean4","match":"'[^\\\\']'"},{"name":"string.quoted.single.lean4","match":"'(\\\\(x[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'","captures":{"1":{"name":"constant.character.escape.lean4"}}},{"name":"entity.name.lean4","match":"`+[^\\[(]\\S+"},{"name":"constant.numeric.lean4","match":"\\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(0|[1-9][0-9]*)(\\.[0-9]+)?([eE][+-]?[0-9]+)?)\\b"}],"repository":{"blockComment":{"name":"comment.block.lean4","begin":"/-","end":"-/","patterns":[{"include":"source.lean4.markdown"},{"include":"#blockComment"}]},"comments":{"patterns":[{"include":"#dashComment"},{"include":"#docComment"},{"include":"#stringBlock"},{"include":"#modDocComment"},{"include":"#blockComment"}]},"dashComment":{"name":"comment.line.double-dash.lean4","begin":"--","end":"$","patterns":[{"include":"source.lean4.markdown"}]},"definitionName":{"patterns":[{"name":"entity.name.function.lean4","match":"\\b[^:«»\\(\\)\\{\\}[:space:]=→λ∀?][^:«»\\(\\)\\{\\}[:space:]]*"},{"contentName":"entity.name.function.lean4","begin":"«","end":"»"}]},"docComment":{"name":"comment.block.documentation.lean4","begin":"/--","end":"-/","patterns":[{"include":"source.lean4.markdown"},{"include":"#blockComment"}]},"modDocComment":{"name":"comment.block.documentation.lean4","begin":"/-!","end":"-/","patterns":[{"include":"source.lean4.markdown"},{"include":"#blockComment"}]}}}