Skip to content

Idris: add Idris 2 keywords, builtins, pragmas, and string interpolation#4063

Open
bio-aeon wants to merge 1 commit intoPrismJS:v2from
bio-aeon:idris2-keywords
Open

Idris: add Idris 2 keywords, builtins, pragmas, and string interpolation#4063
bio-aeon wants to merge 1 commit intoPrismJS:v2from
bio-aeon:idris2-keywords

Conversation

@bio-aeon
Copy link

@bio-aeon bio-aeon commented Mar 6, 2026

Closes #4062.

Brings the Idris grammar up to date with Idris 2 while keeping Idris 1 keywords for backward compatibility.

Changes:

  • Added 9 missing Idris 2 keywords (auto, autobind, covering, default, failing, forall, open, prefix, typebind), cross-referenced with the Idris 2 lexer. Kept all existing Idris 1 keywords so older code still highlights.
  • Moved Type from keyword to builtin and populated the builtin token with common Idris types (Type, Int, Integer, Nat, Double, String, Char, Bool, List, Maybe, IO, Unit, Void).
  • Added a pragma token (/%\w+/) for %default, %inline, %foreign, etc. Uses alias: 'keyword' so pragmas pick up keyword styling with no theme changes.
  • Added \{expr} string interpolation. This meant overriding the inherited Haskell string pattern - used /"(?:[^\\"]|\\[\s\S])*"/ so multiline gap strings still work.

Tests:

  • keyword_feature.test - updated with full keyword list (Idris 1 + 2)
  • string_feature.test - updated expected format (strings now have inside, so content is array-wrapped)
  • builtin_feature.test - new
  • pragma_feature.test - new
  • interpolation_feature.test - new
  • Existing tests for comments, chars, numbers, operators, constants, hvariables, import statements are unaffected

@netlify
Copy link

netlify bot commented Mar 6, 2026

Deploy Preview for dev-prismjs-com ready!

Name Link
🔨 Latest commit b239288
🔍 Latest deploy log https://app.netlify.com/projects/dev-prismjs-com/deploys/69ab50b7520ec100083c3877
😎 Deploy Preview https://deploy-preview-4063--dev-prismjs-com.netlify.app
📱 Preview on mobile
Toggle QR Code...

QR Code

Use your smartphone camera to open QR code link.

To edit notification comments on pull requests, go to your Netlify project configuration.

@github-actions
Copy link

github-actions bot commented Mar 6, 2026

No JS Changes

Generated by 🚫 dangerJS against b239288

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

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

1 participant