{
  "name": "F*",
  "scopeName": "source.fstar",
  "patterns": [
    {
      "include": "#comments"
    },
    {
      "include": "#modules"
    },
    {
      "include": "#options"
    },
    {
      "include": "#expr"
    }
  ],
  "repository": {
    "commentblock": {
      "patterns": [
        {
          "name": "comment.block.fstar",
          "begin": "\\(\\*",
          "end": "\\*\\)",
          "patterns": [
            {
              "include": "#commentblock"
            }
          ],
          "beginCaptures": {
            "0": {
              "name": "punctuation.definition.comment.begin.fstar"
            }
          },
          "endCaptures": {
            "0": {
              "name": "punctuation.definition.comment.end.fstar"
            }
          }
        }
      ]
    },
    "comments": {
      "patterns": [
        {
          "name": "comment.line.fstar",
          "match": "//.*"
        },
        {
          "include": "#commentblock"
        }
      ]
    },
    "expr": {
      "patterns": [
        {
          "include": "#comments"
        },
        {
          "name": "variable.other.generic-type.fstar",
          "match": "'[a-zA-Z0-9_]+\\b"
        },
        {
          "include": "#strings"
        },
        {
          "name": "support.class.base.fstar",
          "match": "\\b(int|nat|pos|bool|unit|string|Type|Type0|eqtype)\\b"
        },
        {
          "name": "support.class.base.fstar",
          "match": "(/\\\\|\\\\/|\u003c:|\u003c@|[(][|]|[|][)]|u#|~\u003e|-\u003e|\u003c--|\u003c-|\u003c==\u003e|==\u003e|[?][.]|[.]\\[|[.]\\(|[{][:]pattern|::|:=|;;|[!][{]|\\[[|]|[|]\u003e|[|]\\]|[~+^\u0026?$|#,.:;=\\[\\](){}-])"
        },
        {
          "name": "constant.language.monad.fstar",
          "match": "\\b(Pure|PURE|Tot|STATE|ST|St|Stack|StackInline|HST|ALL|All|EXN|Exn|Ex|DIV|Div|GHOST|Ghost|GTot|Lemma)\\b"
        },
        {
          "name": "constant.language.fstar",
          "match": "\\b(_|[(]\\s*[)]|\\[\\s*\\])\\b"
        },
        {
          "name": "keyword.other.fstar",
          "match": "\\b(let|in|type|kind|val|rec|and|if|then|else|assume|admit|assert|assert_norm|squash|failwith|SMTPat|SMTPatOr|hasEq|fun|function|forall|exists|exception|by|new_effect|reify|try|synth|with|when)\\b"
        },
        {
          "name": "storage.modifier.fstar",
          "match": "\\b(abstract|attributes|noeq|unopteq|inline|inline_for_extraction|irreducible|logic|mutable|new|noextract|private|reifiable|reflectable|total|unfold|unfoldable)\\b"
        },
        {
          "name": "constant.language.boolean.fstar",
          "match": "\\b([tT]rue|[fF]alse)\\b"
        },
        {
          "name": "constant.numeric.hex.js",
          "match": "\\b0[xX][0-9a-fA-F]+[uU]?[zyslL]?\\b"
        },
        {
          "name": "constant.numeric.decimal.js",
          "match": "\\b[0-9]+[uU]?[zyslL]?\\b"
        },
        {
          "match": "(?x)\n(?:\n  (?:\\b[0-9]+(\\.)[0-9]+[eE][+-]?[0-9]+\\b)| # 1.1E+3\n  (?:\\b[0-9]+(\\.)[eE][+-]?[0-9]+\\b)|       # 1.E+3\n  (?:\\B(\\.)[0-9]+[eE][+-]?[0-9]+\\b)|       # .1E+3\n  (?:\\b[0-9]+[eE][+-]?[0-9]+\\b)|            # 1E+3\n  (?:\\b[0-9]+(\\.)[0-9]+\\b)|                # 1.1\n  (?:\\b[0-9]+(\\.)\\B)|                      # 1.\n  (?:\\B(\\.)[0-9]+\\b)|                      # .1\n  (?:\\b[0-9]+\\b(?!\\.))                     # 1\n)[L]?[fF]?",
          "captures": {
            "0": {
              "name": "constant.numeric.decimal.fstar"
            },
            "1": {
              "name": "meta.delimiter.decimal.period.fstar"
            },
            "2": {
              "name": "meta.delimiter.decimal.period.fstar"
            },
            "3": {
              "name": "meta.delimiter.decimal.period.fstar"
            },
            "4": {
              "name": "meta.delimiter.decimal.period.fstar"
            },
            "5": {
              "name": "meta.delimiter.decimal.period.fstar"
            },
            "6": {
              "name": "meta.delimiter.decimal.period.fstar"
            }
          }
        },
        {
          "begin": "([(])\\s*(requires|ensures|decreases)?",
          "end": "([)])",
          "patterns": [
            {
              "include": "#expr"
            }
          ],
          "beginCaptures": {
            "1": {
              "name": "punctuation.definition.scope.begin.bracket.round.fstar"
            },
            "2": {
              "name": "keyword.other.fstar"
            }
          },
          "endCaptures": {
            "1": {
              "name": "punctuation.definition.scope.end.bracket.round.fstar"
            }
          }
        },
        {
          "begin": "([(])",
          "end": "([)])",
          "patterns": [
            {
              "include": "#expr"
            }
          ],
          "beginCaptures": {
            "1": {
              "name": "punctuation.definition.clause.begin.bracket.round.fstar"
            }
          },
          "endCaptures": {
            "1": {
              "name": "punctuation.definition.clause.end.bracket.round.fstar"
            }
          }
        },
        {
          "begin": "([%]\\[)",
          "end": "(\\])",
          "patterns": [
            {
              "include": "#expr"
            }
          ],
          "beginCaptures": {
            "1": {
              "name": "constant.language.termorder.begin.fstar"
            }
          },
          "endCaptures": {
            "1": {
              "name": "constant.language.termorder.end.fstar"
            }
          }
        },
        {
          "begin": "(\\[[@])",
          "end": "(\\])",
          "patterns": [
            {
              "include": "#expr"
            }
          ],
          "beginCaptures": {
            "1": {
              "name": "storage.modifier.attributes.begin.fstar"
            }
          },
          "endCaptures": {
            "1": {
              "name": "storage.modifier.attributes.end.fstar"
            }
          }
        },
        {
          "begin": "\\b(match)\\b",
          "end": "\\b(with)\\b",
          "patterns": [
            {
              "include": "#expr"
            }
          ],
          "beginCaptures": {
            "1": {
              "name": "keyword.control.match.fstar"
            }
          },
          "endCaptures": {
            "1": {
              "name": "keyword.control.with.fstar"
            }
          }
        },
        {
          "begin": "\\b(begin)\\b",
          "end": "\\b(end)\\b",
          "patterns": [
            {
              "include": "#expr"
            }
          ],
          "beginCaptures": {
            "1": {
              "name": "keyword.control.begin.fstar"
            }
          },
          "endCaptures": {
            "1": {
              "name": "keyword.control.end.fstar"
            }
          }
        },
        {
          "match": "\\b([\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)\\b(?!\\s*[.])",
          "captures": {
            "1": {
              "name": "support.function.constructor.fstar"
            }
          }
        },
        {
          "match": "\\b((?:[\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*[.])+)",
          "captures": {
            "1": {
              "name": "variable.other.module.fstar"
            }
          }
        },
        {
          "match": "\\b([\\p{Ll}_][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)",
          "captures": {
            "1": {
              "name": "entity.name.function.fstar"
            }
          }
        }
      ]
    },
    "modules": {
      "patterns": [
        {
          "begin": "\\b(module)\\s+([\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)\\s*(=)",
          "end": "\\b((?\u003cname\u003e[\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)(?:[.]\\g\u003cname\u003e)*)\\b",
          "beginCaptures": {
            "1": {
              "name": "keyword.control.module.fstar"
            },
            "2": {
              "name": "variable.other.module-alias.fstar"
            },
            "3": {
              "name": "keyword.operator.assignment.fstar"
            }
          },
          "endCaptures": {
            "1": {
              "name": "variable.other.module.fstar"
            }
          }
        },
        {
          "begin": "\\b(module|open|include)\\b",
          "end": "\\b((?\u003cname\u003e[\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)(?:[.]\\g\u003cname\u003e)*)\\b",
          "beginCaptures": {
            "1": {
              "name": "keyword.control.module.fstar"
            }
          },
          "endCaptures": {
            "1": {
              "name": "variable.other.module.fstar"
            }
          }
        }
      ]
    },
    "op_names": {
      "patterns": [
        {
          "name": "entity.name.tag.fstar",
          "match": "\\bop(?:_(?:Multiply|Star|Slash|Percent|Plus|Substraction|Equals|Less|Greater|Bang|Dollar|Amp|Dot|Hat|Colon|Pipe|Question))+\\b"
        }
      ]
    },
    "options": {
      "patterns": [
        {
          "match": "(#(?:re)?set-options)\\s*([\"])((?:[^\"]|\\\\\")*)([\"])",
          "captures": {
            "1": {
              "name": "keyword.control.setoption.fstar"
            },
            "2": {
              "name": "punctuation.definition.options.begin.fstar"
            },
            "3": {
              "name": "string.quoted.double.fstar"
            },
            "4": {
              "name": "punctuation.definition.options.end.fstar"
            }
          }
        }
      ]
    },
    "string_escapes": {
      "patterns": [
        {
          "name": "invalid.illegal.unicode-escape.fstar",
          "match": "\\\\u(?![A-Fa-f0-9]{4}|{[A-Fa-f0-9]+})[^'\"]*"
        },
        {
          "name": "constant.character.escape.js",
          "match": "\\\\u(?:[A-Fa-f0-9]{4}|({)([A-Fa-f0-9]+)(}))",
          "captures": {
            "1": {
              "name": "punctuation.definition.unicode-escape.begin.bracket.curly.fstar"
            },
            "2": {
              "patterns": [
                {
                  "name": "invalid.illegal.unicode-escape.fstar",
                  "match": "[A-Fa-f\\d]{7,}|(?!10)[A-Fa-f\\d]{6}"
                }
              ]
            },
            "3": {
              "name": "punctuation.definition.unicode-escape.end.bracket.curly.fstar"
            }
          }
        },
        {
          "name": "constant.character.escape.fstar",
          "match": "\\\\(x[0-9A-Fa-f]{2}|[0-2][0-7]{0,2}|3[0-6][0-7]?|37[0-7]?|[4-7][0-7]?|.)"
        }
      ]
    },
    "strings": {
      "patterns": [
        {
          "name": "string.quoted.double.fstar",
          "begin": "\"",
          "end": "\"",
          "patterns": [
            {
              "include": "#string_escapes"
            }
          ],
          "beginCaptures": {
            "0": {
              "name": "punctuation.definition.string.begin.fstar"
            }
          },
          "endCaptures": {
            "0": {
              "name": "punctuation.definition.string.end.fstar"
            }
          }
        },
        {
          "name": "string.quoted.single.fstar",
          "begin": "'",
          "end": "'",
          "patterns": [
            {
              "include": "#string_escapes"
            },
            {
              "name": "invalid.illegal.string.js",
              "match": ".{2,}"
            }
          ],
          "beginCaptures": {
            "0": {
              "name": "punctuation.definition.char.begin.fstar"
            }
          },
          "endCaptures": {
            "0": {
              "name": "punctuation.definition.char.end.fstar"
            }
          }
        },
        {
          "name": "string.quoted.template.fstar",
          "begin": "`",
          "end": "`",
          "patterns": [
            {
              "include": "#op_names"
            }
          ],
          "beginCaptures": {
            "0": {
              "name": "punctuation.definition.operator.begin.fstar"
            }
          },
          "endCaptures": {
            "0": {
              "name": "punctuation.definition.operator.end.fstar"
            }
          }
        }
      ]
    }
  }
}