%YAML 1.2
---
# http://www.sublimetext.com/docs/syntax.html
name: Lean 4
file_extensions:
  - lean
scope: source.lean4
contexts:
  main:
    - include: comments
    - match: \b(Prop|Type|Sort)\b
      scope: storage.type.lean4
    - match: '\battribute\b\s*\[[^\]]*\]'
      scope: storage.modifier.lean4
    - match: '@\[[^\]]*\]'
      scope: storage.modifier.lean4
    - match: \b(?<!\.)(global|local|scoped|partial|unsafe|private|protected|noncomputable)(?!\.)\b
      scope: storage.modifier.lean4
    - match: \b(sorry|admit|stop)\b
      scope: invalid.illegal.lean4
    - match: '#(print|eval|reduce|check|check_failure)\b'
      scope: keyword.other.lean4
    - match: \bderiving\s+instance\b
      scope: keyword.other.command.lean4
    - match: '\b(?<!\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\b\s+(\{[^}]*\})?'
      captures:
        1: keyword.other.definitioncommand.lean4
      push:
        - meta_scope: meta.definitioncommand.lean4
        - match: '(?=\bwith\b|\bextends\b|\bwhere\b|[:\|\(\[\{⦃<>])'
          pop: true
        - include: comments
        - include: definitionName
        - match: ','
    - match: \b(?<!\.)(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
      scope: keyword.other.lean4
    - match: «
      push:
        - meta_content_scope: entity.name.lean4
        - match: »
          pop: true
    - match: (s!)"
      captures:
        1: keyword.other.lean4
      push:
        - meta_scope: string.interpolated.lean4
        - match: '"'
          pop: true
        - match: '(\{)'
          captures:
            1: keyword.other.lean4
          push:
            - match: '(\})'
              captures:
                1: keyword.other.lean4
              pop: true
            - include: main
        - match: '\\[\\"ntr'']'
          scope: constant.character.escape.lean4
        - match: '\\x[0-9A-Fa-f][0-9A-Fa-f]'
          scope: constant.character.escape.lean4
        - match: '\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]'
          scope: constant.character.escape.lean4
    - match: '"'
      push:
        - meta_scope: string.quoted.double.lean4
        - match: '"'
          pop: true
        - match: '\\[\\"ntr'']'
          scope: constant.character.escape.lean4
        - match: '\\x[0-9A-Fa-f][0-9A-Fa-f]'
          scope: constant.character.escape.lean4
        - match: '\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]'
          scope: constant.character.escape.lean4
    - match: \b(true|false)\b
      scope: constant.language.lean4
    - match: '''[^\\'']'''
      scope: 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]|.))'''
      scope: string.quoted.single.lean4
      captures:
        1: constant.character.escape.lean4
    - match: '`+[^\[(]\S+'
      scope: entity.name.lean4
    - match: '\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(0|[1-9][0-9]*)(\.[0-9]+)?([eE][+-]?[0-9]+)?)\b'
      scope: constant.numeric.lean4
  blockComment:
    - match: /-
      push:
        - meta_scope: comment.block.lean4
        - match: '-/'
          pop: true
        - include: scope:source.lean4.markdown
        - include: blockComment
  comments:
    - include: dashComment
    - include: docComment
    - include: modDocComment
    - include: blockComment
  dashComment:
    - match: '--'
      push:
        - meta_scope: comment.line.double-dash.lean4
        - match: $
          pop: true
        - include: scope:source.lean4.markdown
  definitionName:
    - match: '\b[^:«»\(\)\{\}[:space:]=→λ∀?][^:«»\(\)\{\}[:space:]]*'
      scope: entity.name.function.lean4
    - match: «
      push:
        - meta_content_scope: entity.name.function.lean4
        - match: »
          pop: true
  docComment:
    - match: /--
      push:
        - meta_scope: comment.block.documentation.lean4
        - match: '-/'
          pop: true
        - include: scope:source.lean4.markdown
        - include: blockComment
  modDocComment:
    - match: /-!
      push:
        - meta_scope: comment.block.documentation.lean4
        - match: '-/'
          pop: true
        - include: scope:source.lean4.markdown
        - include: blockComment