Syntax Highlighting for Key files usable by bat

key.sublime-syntax

%YAML 1.2
---
name: KeY
file_extensions: [key]
scope: source.key

contexts:
  main:
    - match: '"'
      scope: punctuation.definition.string.begin
      push: double_quoted_string
    
#    # global key words
#    - match: '\b(if|else|for|while)\b'
#      scope: keyword.control.example-c

    - match: '\b\\(javaSource\|chooseContract\|proofObligation\|bootclasspath\|problem\|programVariables)\b(.*)?;'
      captures:
        1: keyword


    # Numbers
    - match: '\b(-)?[0-9.]+\b'
      scope: constant.numeric.example-c

    - match: '(\\sorts)\s*\{'
      captures:
        1: keyword.group
      push: insideSort

    - match: '(\\predicates)\s*\{'
      captures:
        1: keyword.group
      push: insidePredicates

    - match: '(\\functions)\s*\{'
      captures:
        1: keyword.group
      push: insideFunctions       

    - match: '(\\schemaVariables)\s*\{'
      captures:
        1: keyword.group
      push: insideFunctions       

    - match: '(\\rules)\s*\{'
      captures:
        1: keyword.group
      push: insideRules       


    - include: all

  all:
    - match: '//'
      scope: punctuation.definition.comment
      push: line_comment

    - match: '/\*'
      scope: punctuation.definition.comment.begin
      push: multi_comment


  double_quoted_string:
    - meta_scope: string.quoted.double
    - match: '\\.'
      scope: constant.character.escape
    - match: '"'
      scope: punctuation.definition.string.end.example-c
      pop: true

  line_comment:
    - meta_scope: comment.line
    - match: $
      pop: true

  multi_comment:
    - meta_scope: comment.block
    - match: '\*/'
      pop: true

  insideSort:
    - include: all
    - match: '((\w|\\)+)(;)'
      captures:
        1: entity.name.type
        3: punctuation.terminator        
    - match: '\}'
      pop: true

  insideFunctions:
    - include: all
    - match: '\\unique'
      scope: keyword
    - match: '((\w|\\)+)\s+((\w|\\)+)\s*(;)'
      captures:
        1: entity.name.type
        3: variable.function
        5: punctuation.terminator
    - match: '((\w|\\)+)\s+((\w|\\)+)(\{.*\})?\s*\('
      captures:
        1: entity.name.type
        3: variable.function
        5: variable.function
      push: sortArgs
    - match: ';'
      scope: punctuation.terminator
    - match: '\}'
      pop: true

  sortArgs:
    - match: '\b\b((\w|\\)+)\b'
      scope: entity.name.type
    - match: '\)'
      pop: true

  insidePredicates:
    - match: '\}'
      pop: true

  insideRules:
    - include: all
    - match: '(\w+)\s*\{'
      push: insideRule
      captures:
        1: keyword      
    - match: '\}'
      pop: true

  insideRule:
    - match: '(\\schemaVar) ((\w|\\)+) ((\w|\\)+) ((\w|\\)+)(;)'
      captures:
        1: keyword
        2: keyword
        3: entity.name.type
        4: variable    
    - match: '\W\\(find|if|then|else|assumes|modality|replacewith|add|heuristics|endmodality|varcond|not|hasSort|isThisReference|staticMethodReference|displayname|sameUpdateLevel|schemaVar|modalOperator|new|typeof|term|update|formula)\W'
      scope: keyword
    - match: '\};'
      pop: true