{
  "name": "TLA",
  "scopeName": "source.tla",
  "patterns": [
    {
      "name": "comment.line.slash-star",
      "match": "\\\\\\*.*$"
    },
    {
      "name": "comment.block",
      "begin": "\\(\\*",
      "end": "\\*\\)"
    },
    {
      "name": "markup.other.startbreak",
      "match": "\\={4,}"
    },
    {
      "name": "markup.other.endbreak",
      "match": "={4,}"
    },
    {
      "name": "constant.numeric",
      "match": "\\b(\\\\h[0-9a-fA-F]+|\\\\o[0-9]+|\\\\b[01]+|\\d+\\.\\d+|\\d+)\\b"
    },
    {
      "name": "constant.language.tla",
      "match": "\\b(BOOLEAN|FALSE|STRING|TRUE)\\b"
    },
    {
      "name": "keyword.operator.definition.tla",
      "match": "\\b==\\b"
    },
    {
      "name": "keyword.operator.logic.tla",
      "match": "(\\/\\\\|\\\\\\/|\\=\u003e|\u003c\\=\u003e|\\|\\=|\\=\\||\\|\\-|\\-\\||~)"
    },
    {
      "name": "keyword.operator.comparison.tla",
      "match": "\u003c\\=|\u003e\\=|\\=|\u003c|\u003e|\\/\\=|\\#"
    },
    {
      "name": "keyword.operator.assignment.tla",
      "match": "\\b=\\b"
    },
    {
      "name": "keyword.operator.temporal.quantification.tla",
      "match": "(\\\\EE|\\\\AA)"
    },
    {
      "name": "keyword.operator.quantification.tla",
      "match": "(\\\\E|\\\\A)"
    },
    {
      "name": "keyword.operator.sets.tla",
      "match": "(\\\\notin|:)"
    },
    {
      "name": "keyword.operator.functions.tla",
      "match": "(\\|\\-\u003e|\\-\u003e)"
    },
    {
      "name": "keyword.operator.latex.tla",
      "match": "\\\\(approx|asymp|bigcirc|bullet|cap|cdot|circ|cong|cup|div|doteq|equiv|geq|gg|in|intersect|land|leq|ll|lor|o|odot|ominus|oplus|oslash|otimes|prec|preceq|propto|sim|simeq|sqcap|sqcup|sqsubset|sqsubseteq|sqsupset|sqsupseteq|star|subset|subseteq|succ|succeq|supset|supseteq|union|uplus|wr)\\b"
    },
    {
      "name": "keyword.operator.arithmetic.tla",
      "match": "\\b(\\+|\\-|\\*|\\/){1}\\b"
    },
    {
      "name": "keyword.operator.temporal.tla",
      "match": "(\\[\\]|\\\u003c\\\u003e|\\-\\+\\-\u003e)"
    },
    {
      "include": "#reserved-words"
    },
    {
      "name": "string.quoted.double.tla",
      "begin": "\"",
      "end": "\""
    },
    {
      "name": "string.quoted.single.tla",
      "begin": "';\n\t\t\tend = '"
    },
    {
      "name": "meta.structure.list.tla",
      "begin": "(\\[)",
      "end": "(\\])",
      "patterns": [
        {
          "contentName": "meta.structure.list.item.tla",
          "begin": "(?\u003c=\\[|\\,)\\s*(?![\\],])",
          "end": "\\s*(?:(,)|(?=\\]))",
          "patterns": [
            {
              "include": "$self"
            }
          ],
          "endCaptures": {
            "1": {
              "name": "punctuation.separator.list.tla"
            }
          }
        }
      ],
      "beginCaptures": {
        "1": {
          "name": "punctuation.definition.list.begin.tla"
        }
      },
      "endCaptures": {
        "1": {
          "name": "punctuation.definition.list.end.tla"
        }
      }
    },
    {
      "name": "meta.structure.tuple.tla",
      "match": "(\u003c\u003c)(\\s*(\u003e\u003e))",
      "captures": {
        "1": {
          "name": "punctuation.definition.tuple.begin.tla"
        },
        "2": {
          "name": "meta.empty-tuple.tla"
        },
        "3": {
          "name": "punctuation.definition.tuple.end.tla"
        }
      }
    }
  ],
  "repository": {
    "reserved-words": {
      "name": "keyword.control.tla",
      "match": "\\b(ACTION|ASSUME|ASSUMPTION|AXIOM|BY|CASE|CHOOSE|CONSTANT|CONSTANTS|COROLLARY|DEF|DEFINE|DEFS|DOMAIN|ELSE|ENABLED|EXCEPT|EXTENDS|HAVE|HIDE|IF|IN|INSTANCE|LAMBDA|LEMMA|LET|LOCAL|MODULE|NEW|OBVIOUS|OMITTED|ONLY|OTHER|PICK|PROOF|PROPOSITION|PROVE|QED|RECURSIVE|SF_|STATE|SUBSET|SUFFICES|TAKE|TEMPORAL|THEN|THEOREM|UNCHANGED|UNION|USE|VARIABLE|VARIABLES|WF_|WITH|WITNESS)\\b"
    }
  }
}