{
  "name": "Idris",
  "scopeName": "source.idris",
  "patterns": [
    {
      "name": "keyword.operator.function.infix.idris",
      "match": "(`)[\\w']*?(`)",
      "captures": {
        "1": {
          "name": "punctuation.definition.entity.idris"
        },
        "2": {
          "name": "punctuation.definition.entity.idris"
        }
      }
    },
    {
      "name": "meta.declaration.module.idris",
      "match": "^(module)\\s+([a-zA-Z._']+)$",
      "captures": {
        "1": {
          "name": "keyword.other.idris"
        }
      }
    },
    {
      "name": "meta.import.idris",
      "match": "^(import)\\s+([a-zA-Z._']+)$",
      "captures": {
        "1": {
          "name": "keyword.other.idris"
        }
      }
    },
    {
      "name": "constant.numeric.float.idris",
      "match": "\\b([0-9]+\\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\\b"
    },
    {
      "name": "constant.numeric.idris",
      "match": "\\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\\b"
    },
    {
      "name": "storage.modifier.export.idris",
      "match": "^\\b(public|abstract|private)\\b"
    },
    {
      "name": "storage.modifier.totality.idris",
      "match": "\\b(total|partial)\\b"
    },
    {
      "name": "storage.modifier.idris",
      "match": "^\\b(implicit)\\b"
    },
    {
      "name": "string.quoted.double.idris",
      "begin": "\\\"",
      "end": "\\\"",
      "patterns": [
        {
          "include": "#escape_characters"
        }
      ],
      "beginCaptures": {
        "0": {
          "name": "punctuation.definition.string.begin.idris"
        }
      },
      "endCaptures": {
        "0": {
          "name": "punctuation.definition.string.end.idris"
        }
      }
    },
    {
      "name": "string.quoted.single.idris",
      "begin": "(?\u003c!\\w)\\'",
      "end": "\\'",
      "patterns": [
        {
          "include": "#escape_characters"
        },
        {
          "name": "invalid.illegal.idris",
          "match": "\\n"
        }
      ],
      "beginCaptures": {
        "0": {
          "name": "punctuation.definition.string.begin.idris"
        }
      },
      "endCaptures": {
        "0": {
          "name": "punctuation.definition.string.end.idris"
        }
      }
    },
    {
      "name": "meta.declaration.class.idris",
      "begin": "\\b(class)\\b",
      "end": "\\b(where)\\b|$",
      "patterns": [
        {
          "include": "#prelude_class"
        },
        {
          "include": "#prelude_type"
        }
      ],
      "beginCaptures": {
        "1": {
          "name": "keyword.other.idris"
        }
      },
      "endCaptures": {
        "1": {
          "name": "keyword.other.idris"
        }
      }
    },
    {
      "name": "meta.declaration.instance.idris",
      "begin": "\\b(instance)\\b",
      "end": "\\b(where)\\b|$",
      "patterns": [
        {
          "include": "#prelude_class"
        },
        {
          "include": "#prelude_type"
        },
        {
          "include": "#context_signature"
        },
        {
          "include": "#type_signature"
        }
      ],
      "beginCaptures": {
        "1": {
          "name": "keyword.other.idris"
        }
      },
      "endCaptures": {
        "1": {
          "name": "keyword.other.idris"
        }
      }
    },
    {
      "name": "meta.declaration.data.idris",
      "begin": "\\b(data)\\s+([\\w']+)\\s*(:)?",
      "end": "\\b(where)\\b|(=)",
      "patterns": [
        {
          "include": "#type_signature"
        }
      ],
      "beginCaptures": {
        "1": {
          "name": "keyword.other.idris"
        },
        "2": {
          "name": "entity.name.type.idris"
        },
        "3": {
          "name": "keyword.operator.colon.idris"
        }
      },
      "endCaptures": {
        "1": {
          "name": "keyword.other.idris"
        },
        "2": {
          "name": "keyword.operator.idris"
        }
      }
    },
    {
      "include": "#function_signature"
    },
    {
      "include": "#directive"
    },
    {
      "include": "#comments"
    },
    {
      "include": "#language_const"
    },
    {
      "include": "#language_keyword"
    },
    {
      "include": "#prelude"
    },
    {
      "name": "constant.other.idris",
      "match": "\\b[A-Z][A-Za-z_'0-9]*"
    },
    {
      "name": "keyword.operator.idris",
      "match": "[|\u0026!%$?~+:\\-.=\u003c/\u003e\\\\*]+"
    },
    {
      "name": "punctuation.separator.comma.idris",
      "match": ","
    }
  ],
  "repository": {
    "block_comment": {
      "name": "comment.block.idris",
      "begin": "\\{-(?!#)",
      "end": "-\\}",
      "patterns": [
        {
          "include": "#block_comment"
        }
      ],
      "captures": {
        "0": {
          "name": "punctuation.definition.comment.idris"
        }
      }
    },
    "comments": {
      "patterns": [
        {
          "name": "comment.line.double-dash.idris",
          "match": "(--).*$\\n?",
          "captures": {
            "1": {
              "name": "punctuation.definition.comment.idris"
            }
          }
        },
        {
          "name": "comment.line.triple-bar.idris",
          "match": "(\\|\\|\\|).*$\\n?",
          "captures": {
            "1": {
              "name": "punctuation.definition.comment.idris"
            }
          }
        },
        {
          "include": "#block_comment"
        }
      ]
    },
    "context_signature": {
      "patterns": [
        {
          "name": "meta.context-signature.idris",
          "match": "([\\w._']+)((\\s+[\\w_']+)+)\\s*(=\u003e)",
          "captures": {
            "1": {
              "name": "entity.other.inherited-class.idris"
            },
            "2": {
              "name": "entity.other.attribute-name.idris"
            },
            "4": {
              "name": "keyword.operator.double-arrow.idris"
            }
          }
        },
        {
          "name": "meta.context-signature.idris",
          "begin": "(\\()((?=.*\\)\\s*=\u003e)|(?=[^)]*$))",
          "end": "(\\))\\s*(=\u003e)",
          "patterns": [
            {
              "name": "meta.class-constraint.idris",
              "match": "([\\w']+)\\s+([\\w']+)",
              "captures": {
                "1": {
                  "name": "entity.other.inherited-class.idris"
                },
                "2": {
                  "name": "entity.other.attribute-name.idris"
                }
              }
            }
          ],
          "beginCaptures": {
            "1": {
              "name": "punctuation.context.begin.idris"
            }
          },
          "endCaptures": {
            "1": {
              "name": "punctuation.context.end.idris"
            },
            "2": {
              "name": "keyword.operator.double-arrow.idris"
            }
          }
        }
      ]
    },
    "directive": {
      "patterns": [
        {
          "name": "meta.directive.language-extension.idris",
          "match": "^%(language)\\s+(.*)$",
          "captures": {
            "1": {
              "name": "keyword.other.directive.idris"
            },
            "2": {
              "name": "keyword.other.language-extension.idris"
            }
          }
        },
        {
          "name": "meta.directive.totality.idris",
          "match": "^%(default)\\s+(total|partial)$",
          "captures": {
            "1": {
              "name": "keyword.other.directive.idris"
            },
            "2": {
              "name": "keyword.other.totality.idris"
            }
          }
        },
        {
          "name": "meta.directive.type-provider.idris",
          "match": "^%(provide)\\s+.*\\s+(with)\\s+.*$",
          "captures": {
            "1": {
              "name": "keyword.other.directive.idris"
            },
            "2": {
              "name": "keyword.other.idris"
            }
          }
        },
        {
          "name": "meta.directive.export.idris",
          "match": "^%(access)\\s+(public|abstract|private)$",
          "captures": {
            "1": {
              "name": "keyword.other.directive.idris"
            },
            "2": {
              "name": "storage.modifier.export.idris"
            }
          }
        },
        {
          "name": "meta.directive.idris",
          "match": "^%([\\w]+)\\b",
          "captures": {
            "1": {
              "name": "keyword.other.directive.idris"
            }
          }
        }
      ]
    },
    "escape_characters": {
      "patterns": [
        {
          "name": "constant.character.escape.ascii.idris",
          "match": "\\\\(NUL|SOH|STX|ETX|EOT|ENQ|ACK|BEL|BS|HT|LF|VT|FF|CR|SO|SI|DLE|DC1|DC2|DC3|DC4|NAK|SYN|ETB|CAN|EM|SUB|ESC|FS|GS|RS|US|SP|DEL|[abfnrtv\\\\\\\"'\\\u0026])"
        },
        {
          "name": "constant.character.escape.octal.idris",
          "match": "\\\\o[0-7]+|\\\\x[0-9A-Fa-f]+|\\\\[0-9]+"
        },
        {
          "name": "constant.character.escape.control.idris",
          "match": "\\^[A-Z@\\[\\]\\\\\\^_]"
        }
      ]
    },
    "function_signature": {
      "name": "meta.function.type-signature.idris",
      "begin": "(([\\w']+)|\\(([|!%$+\\-.,=\u003c/\u003e:]+)\\))\\s*(:)(?!:)",
      "end": "(;|(?\u003c=[^\\s\u003e])\\s*(?!-\u003e)\\s*$)",
      "patterns": [
        {
          "include": "#type_signature"
        }
      ],
      "beginCaptures": {
        "2": {
          "name": "entity.name.function.idris"
        },
        "3": {
          "name": "entity.name.function.idris"
        },
        "4": {
          "name": "keyword.operator.colon.idris"
        }
      }
    },
    "language_const": {
      "patterns": [
        {
          "name": "constant.language.unit.idris",
          "match": "\\(\\)"
        },
        {
          "name": "constant.language.bottom.idris",
          "match": "_\\|_"
        },
        {
          "name": "constant.language.underscore.idris",
          "match": "\\b_\\b"
        }
      ]
    },
    "language_keyword": {
      "patterns": [
        {
          "name": "keyword.other.idris",
          "match": "\\b(infix[lr]?|let|where|of|with)\\b"
        },
        {
          "name": "keyword.control.idris",
          "match": "\\b(do|if|then|else|case|in)\\b"
        }
      ]
    },
    "parameter_type": {
      "patterns": [
        {
          "include": "#prelude_type"
        },
        {
          "name": "meta.parameter.named.idris",
          "begin": "\\(([\\w']+)\\s*:(?!:)",
          "end": "\\)",
          "patterns": [
            {
              "include": "#prelude_type"
            }
          ],
          "beginCaptures": {
            "1": {
              "name": "entity.name.tag.idris"
            }
          }
        },
        {
          "name": "meta.parameter.implicit.idris",
          "begin": "\\{((auto|default .+)\\s+)?([\\w']+)\\s*:(?!:)",
          "end": "\\}",
          "patterns": [
            {
              "include": "#prelude_type"
            }
          ],
          "beginCaptures": {
            "1": {
              "name": "storage.modifier.idris"
            },
            "3": {
              "name": "entity.name.tag.idris"
            }
          }
        }
      ]
    },
    "prelude": {
      "patterns": [
        {
          "include": "#prelude_class"
        },
        {
          "include": "#prelude_type"
        },
        {
          "include": "#prelude_function"
        },
        {
          "include": "#prelude_const"
        }
      ]
    },
    "prelude_class": {
      "name": "support.class.prelude.idris",
      "match": "\\b(Eq|Ord|Num|MinBound|MaxBound|Integral|Applicative|Alternative|Cast|Foldable|Functor|Monad|Traversable|Uninhabited|Semigroup|VerifiedSemigroup|Monoid|VerifiedMonoid|Group|VerifiedGroup|AbelianGroup|VerifiedAbelianGroup|Ring|VerifiedRing|RingWithUnity|VerifiedRingWithUnity|JoinSemilattice|VerifiedJoinSemilattice|MeetSemilattice|VerifiedMeetSemilattice|BoundedJoinSemilattice|VerifiedBoundedJoinSemilattice|BoundedMeetSemilattice|VerifiedBoundedMeetSemilattice|Lattice|VerifiedLattice|BoundedLattice|VerifiedBoundedLattice)\\b"
    },
    "prelude_const": {
      "patterns": [
        {
          "name": "support.constant.prelude.idris",
          "match": "\\b(Just|Nothing|Left|Right|True|False|LT|EQ|GT)\\b"
        }
      ]
    },
    "prelude_function": {
      "name": "support.function.prelude.idris",
      "match": "\\b(abs|acos|all|and|any|asin|atan|atan2|break|ceiling|compare|concat|concatMap|const|cos|cosh|curry|cycle|div|drop|dropWhile|elem|encodeFloat|enumFrom|enumFromThen|enumFromThenTo|enumFromTo|exp|fail|filter|flip|floor|foldl|foldl1|foldr|foldr1|fromInteger|fst|gcd|getChar|getLine|head|id|init|iterate|last|lcm|length|lines|log|lookup|map|max|maxBound|maximum|maybe|min|minBound|minimum|mod|negate|not|null|or|pi|pred|print|product|putChar|putStr|putStrLn|readFile|recip|repeat|replicate|return|reverse|scanl|scanl1|sequence|sequence_|show|sin|sinh|snd|span|splitAt|sqrt|succ|sum|tail|take|takeWhile|tan|tanh|uncurry|unlines|unwords|unzip|unzip3|words|writeFile|zip|zip3|zipWith|zipWith3)\\b"
    },
    "prelude_type": {
      "name": "support.type.prelude.idris",
      "match": "\\b(Type|Exists|World|IO|IntTy|FTy|Foreign|File|Mode|Dec|Bool|so|Ordering|Either|Fin|IsJust|List|Maybe|Nat|LTE|GTE|GT|LT|Stream|StrM|Vect|Not|Lazy|Inf|FalseElim)\\b"
    },
    "type_signature": {
      "patterns": [
        {
          "include": "#context_signature"
        },
        {
          "include": "#parameter_type"
        },
        {
          "include": "#language_const"
        },
        {
          "name": "keyword.operator.arrow.idris",
          "match": "-\u003e"
        }
      ]
    }
  }
}