Practical Verification System (PVS) Sublime Text Syntax Highlighting

pvs.sublime-syntax

%YAML 1.2
---
# See http://www.sublimetext.com/docs/3/syntax.html
file_extensions:
  - pvs
scope: source.pvs

contexts:
  # The prototype context is prepended to all contexts but those setting
  # meta_include_prototype: false.
  prototype:
    - include: comments
    - include: match-operators

  main:
    # The main context is the initial starting point of our syntax.
    # Include other contexts from here (or specify them directly).
    - include: keywords
    - include: numbers
    - include: strings

  keywords:
    # http://pvs.csl.sri.com/doc/pvs-language-reference.pdf
    - match: '\b(CODATATYPE|ENDTABLE|JUDGEMENT|SUBLEMMA|CLOSURE|ENDIF|INDUCTIVE|RECURSIVE|CHALLENGE|ENDCASES|IMPORTING|POSTULATE|CLAIM|ENDCOND|IN|PROPOSITION|BY|END|IFF|OR|WITH|CASES|ENDASSUMING|IMPLIES|ORELSE|XOR|BEGIN|ELSE|HAS_TYPE|OBLIGATION|WHEN|BUT|ELSIF|IF|OF|WHERE|AUTO_REWRITE\-|COROLLARY|FUNCTION|NOT|TYPE\+|AXIOM|DATATYPE|GHOST|O|VAR|AUTO_REWRITE\+|CORECURSIVE|FROM|NONEMPTY_TYPE|TYPE|AUTO_REWRITE|CONVERSION\-|FORMULA|MEASURE|TRUE|ASSUMPTION|CONVERSION\+|FORALL|MACRO|THEORY|ASSUMING|CONVERSION|FALSE|LIBRARY|THEOREM|AS|CONTAINING|FACT|LET|THEN|LAW|SUBTYPE_OF|ARRAY|EXPRESSION|LEMMA|TABLEANDTHEN|COND|EXPORTING|CONJECTURE|AND|COINDUCTIVE|EXISTS|LAMBDA|SUBTYPES)\b'
      scope: keyword.control.pvs

  match-operators: [
    {match: '=', scope: keyword.operator.pvs},
    {match: '->', scope: keyword.operator.pvs},
    {match: ':', scope: keyword.operator.pvs}]

  numbers:
    - match: '\b(-)?[0-9.]+\b'
      scope: constant.numeric.pvs

  strings:
    # Strings begin and end with quotes, and use backslashes as an escape
    # character.
    - match: '"'
      scope: punctuation.definition.string.begin.pvs
      push: inside_string

  inside_string:
    - meta_include_prototype: false
    - meta_scope: string.quoted.double.pvs
    - match: '\.'
      scope: constant.character.escape.pvs
    - match: '"'
      scope: punctuation.definition.string.end.pvs
      pop: true

  comments:
    - match: '%'
      scope: punctuation.definition.comment.pvs
      push:
        # This is an anonymous context push for brevity.
        - meta_scope: comment.line.double-slash.pvs
        - match: $\n?
          pop: true

I don't know anything about making Sublime text syntax definitions so this is kind of garbage, but it makes the code at least a bit readable.

Any improvements welcome!