ITADN

Idris: missing Idris 2 keywords, pragmas, builtins, and string interpolation

#4062Openbio-aeon 创建于 2026-03-06
language-definitions
B
bio-aeoncommented
**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 条评论