lean.sublime-syntax (4123B)
1 %YAML 1.2 2 --- 3 # http://www.sublimetext.com/docs/3/syntax.html 4 name: Lean 5 file_extensions: 6 - lean 7 scope: source.lean 8 contexts: 9 main: 10 - include: comments 11 - match: '\b(?<!\.)(inductive|coinductive|structure|theorem|axiom|axioms|abbreviation|lemma|definition|def|instance|class|constant)\b\s+(\{[^}]*\})?' 12 captures: 13 1: keyword.other.definitioncommand.lean 14 push: 15 - meta_scope: meta.definitioncommand.lean 16 - match: '(?=\bwith\b|\bextends\b|[:\|\(\[\{⦃<>])' 17 pop: true 18 - include: comments 19 - include: definitionName 20 - match: "," 21 - match: \b(Prop|Type|Sort)\b 22 scope: storage.type.lean 23 - match: '\battribute\b\s*\[[^\]]*\]' 24 scope: storage.modifier.lean 25 - match: '@\[[^\]]*\]' 26 scope: storage.modifier.lean 27 - match: \b(?<!\.)(private|meta|mutual|protected|noncomputable)\b 28 scope: keyword.control.definition.modifier.lean 29 - match: \b(sorry)\b 30 scope: invalid.illegal.lean 31 - match: '#print\s+(def|definition|inductive|instance|structure|axiom|axioms|class)\b' 32 scope: keyword.other.command.lean 33 - match: '#(print|eval|reduce|check|help|exit|find|where)\b' 34 scope: keyword.other.command.lean 35 - match: \b(?<!\.)(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 36 scope: keyword.other.lean 37 - match: \b(?<!\.)(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from|λ)(?!\.)\b 38 scope: keyword.other.lean 39 - match: « 40 push: 41 - meta_content_scope: entity.name.lean 42 - match: » 43 pop: true 44 - match: \b(?<!\.)(if|then|else)\b 45 scope: keyword.control.lean 46 - match: '"' 47 captures: 48 0: punctuation.definition.string.begin.lean 49 push: 50 - meta_scope: string.quoted.double.lean 51 - match: '"' 52 captures: 53 0: punctuation.definition.string.end.lean 54 pop: true 55 - match: '\\[\\"nt'']' 56 scope: constant.character.escape.lean 57 - match: '\\x[0-9A-Fa-f][0-9A-Fa-f]' 58 scope: constant.character.escape.lean 59 - match: '\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]' 60 scope: constant.character.escape.lean 61 - match: '''[^\\'']''' 62 scope: string.quoted.single.lean 63 - match: '''(\\(x..|u....|.))''' 64 scope: string.quoted.single.lean 65 captures: 66 1: constant.character.escape.lean 67 - match: '`+[^\[(]\S+' 68 scope: entity.name.lean 69 - match: '\b([0-9]+|0([xX][0-9a-fA-F]+))\b' 70 scope: constant.numeric.lean 71 blockComment: 72 - match: /- 73 push: 74 - meta_scope: comment.block.lean 75 - match: "-/" 76 pop: true 77 - include: blockComment 78 comments: 79 - include: dashComment 80 - include: docComment 81 - include: modDocComment 82 - include: blockComment 83 dashComment: 84 - match: (--) 85 captures: 86 0: punctuation.definition.comment.lean 87 push: 88 - meta_scope: comment.line.double-dash.lean 89 - match: $ 90 pop: true 91 definitionName: 92 - match: '\b[^:«»\(\)\{\}[:space:]=→λ∀?][^:«»\(\)\{\}[:space:]]*' 93 scope: entity.name.function.lean 94 - match: « 95 push: 96 - meta_content_scope: entity.name.function.lean 97 - match: » 98 pop: true 99 docComment: 100 - match: /-- 101 push: 102 - meta_scope: comment.block.documentation.lean 103 - match: "-/" 104 pop: true 105 - include: scope:source.lean.markdown 106 - include: blockComment 107 modDocComment: 108 - match: /-! 109 push: 110 - meta_scope: comment.block.documentation.lean 111 - match: "-/" 112 pop: true 113 - include: scope:source.lean.markdown 114 - include: blockComment