Idris: missing Idris 2 keywords, pragmas, builtins, and string interpolation
language-definitions
**Information**
- Language: Idris
- Plugins: none
**Description**
The Idris grammar is missing several Idris 2 features:
1. **Missing keywords.** 9 keywords from Idris 2 aren't recognized: `auto`, `autobind`, `covering`, `default`, `failing`, `forall`, `open`, `prefix`, `typebind`. (Cross-referenced with the [Idris 2 lexer source](https://github.com/idris-lang/Idris2/blob/main/src/Parser/Lexer/Source.idr).)
2. **`Type` classified as keyword.** `Type` is a built-in type constructor, not a reserved keyword. It should be highlighted as a builtin. The grammar currently disables the inherited Haskell `builtin` token entirely (`'builtin': undefined`), but Idris has its own common built-in types (`Type`, `Int`, `Integer`, `Nat`, `String`, `IO`, etc.) that should go there.
3. **No `%`-pragma highlighting.** Idris 2 uses `%`-prefixed pragmas heavily (`%default total`, `%inline`, `%foreign`, `%hint`, `%hide`, `%runElab`, etc.) and none of them get highlighted.
4. **No string interpolation.** Idris 2 supports `\{expr}` interpolation inside double-quoted strings and it's not recognized.
**Code snippet**
[Test page]()
<details>
<summary>The code being highlighted incorrectly.</summary>
```idris
-- keywords `covering`, `failing`, `forall` not highlighted
covering
myFunc : forall a. a -> a
-- pragmas not highlighted at all
%default total
%inline
%foreign "C:puts,libc"
-- Type highlighted as keyword instead of builtin
myId : Type -> Type
-- string interpolation not highlighted
greeting : String -> String
greeting name = "hello \{name}"
```
</details>
0 条评论