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

[bio-aeon]

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.)

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

The code being highlighted incorrectly.

-- 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}"