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

src/languages/idris.js

@@ -10,10 +10,28 @@ export default {
 			'comment': {
 				pattern: /(?:(?:--|\|\|\|).*$|\{-[\s\S]*?-\})/m,
 			},
+			'string': {
+				pattern: /"(?:[^\\"]|\\[\s\S])*"/,
+				greedy: true,
+				inside: {
+					'interpolation': {
+						pattern: /\\\{[^}]*\}/,
+						inside: {
+							'punctuation': /^\\\{|\}$/,
+						},
+					},
+				},
+			},
 			'keyword':
-				/\b(?:Type|case|class|codata|constructor|corecord|data|do|dsl|else|export|if|implementation|implicit|import|impossible|in|infix|infixl|infixr|instance|interface|let|module|mutual|namespace|of|parameters|partial|postulate|private|proof|public|quoteGoal|record|rewrite|syntax|then|total|using|where|with)\b/,
-			'builtin': undefined,
+				/\b(?:auto|autobind|case|class|codata|constructor|corecord|covering|data|default|do|dsl|else|export|failing|forall|if|implementation|implicit|import|impossible|in|infix|infixl|infixr|instance|interface|let|module|mutual|namespace|of|open|parameters|partial|postulate|prefix|private|proof|public|quoteGoal|record|rewrite|syntax|then|total|typebind|using|where|with)\b/,
+			'builtin':
+				/\b(?:Bool|Char|Double|IO|Int|Integer|List|Maybe|Nat|String|Type|Unit|Void)\b/,
 			$insert: {
+				'pragma': {
+					$before: 'keyword',
+					pattern: /%\w+/,
+					alias: 'keyword',
+				},
 				'import-statement': {
 					$before: 'keyword',
 					pattern: /(^\s*import\s+)(?:[A-Z][\w']*)(?:\.[A-Z][\w']*)*/m,

tests/languages/idris/builtin_feature.test

@@ -0,0 +1,35 @@
+Bool
+Char
+Double
+IO
+Int
+Integer
+List
+Maybe
+Nat
+String
+Type
+Unit
+Void
+
+----------------------------------------------------
+
+[
+	["builtin", "Bool"],
+	["builtin", "Char"],
+	["builtin", "Double"],
+	["builtin", "IO"],
+	["builtin", "Int"],
+	["builtin", "Integer"],
+	["builtin", "List"],
+	["builtin", "Maybe"],
+	["builtin", "Nat"],
+	["builtin", "String"],
+	["builtin", "Type"],
+	["builtin", "Unit"],
+	["builtin", "Void"]
+]
+
+----------------------------------------------------
+
+Checks for built-in type constructors.

tests/languages/idris/interpolation_feature.test

@@ -0,0 +1,29 @@
+"hello \{name}"
+"sum: \{show (x + y)}"
+
+----------------------------------------------------
+
+[
+	["string", [
+		"\"hello ",
+		["interpolation", [
+			["punctuation", "\\{"],
+			"name",
+			["punctuation", "}"]
+		]],
+		"\""
+	]],
+	["string", [
+		"\"sum: ",
+		["interpolation", [
+			["punctuation", "\\{"],
+			"show (x + y)",
+			["punctuation", "}"]
+		]],
+		"\""
+	]]
+]
+
+----------------------------------------------------
+
+Checks for string interpolation with \{expr}.

tests/languages/idris/keyword_feature.test

@@ -1,14 +1,19 @@
-Type
+auto
+autobind
 case
 class
 codata
 constructor
 corecord
+covering
 data
+default
 do
 dsl
 else
 export
+failing
+forall
 if
 implementation
 implicit
@@ -25,9 +30,11 @@ module
 mutual
 namespace
 of
+open
 parameters
 partial
 postulate
+prefix
 private
 proof
 public
@@ -37,24 +44,30 @@ rewrite
 syntax
 then
 total
+typebind
 using
 where
 with
 
 ----------------------------------------------------
 
 [
-	["keyword", "Type"],
+	["keyword", "auto"],
+	["keyword", "autobind"],
 	["keyword", "case"],
 	["keyword", "class"],
 	["keyword", "codata"],
 	["keyword", "constructor"],
 	["keyword", "corecord"],
+	["keyword", "covering"],
 	["keyword", "data"],
+	["keyword", "default"],
 	["keyword", "do"],
 	["keyword", "dsl"],
 	["keyword", "else"],
 	["keyword", "export"],
+	["keyword", "failing"],
+	["keyword", "forall"],
 	["keyword", "if"],
 	["keyword", "implementation"],
 	["keyword", "implicit"],
@@ -71,9 +84,11 @@ with
 	["keyword", "mutual"],
 	["keyword", "namespace"],
 	["keyword", "of"],
+	["keyword", "open"],
 	["keyword", "parameters"],
 	["keyword", "partial"],
 	["keyword", "postulate"],
+	["keyword", "prefix"],
 	["keyword", "private"],
 	["keyword", "proof"],
 	["keyword", "public"],
@@ -83,11 +98,12 @@ with
 	["keyword", "syntax"],
 	["keyword", "then"],
 	["keyword", "total"],
+	["keyword", "typebind"],
 	["keyword", "using"],
 	["keyword", "where"],
 	["keyword", "with"]
 ]
 
 ----------------------------------------------------
 
-Checks for some keywords.
+Checks for keywords.

tests/languages/idris/pragma_feature.test

@@ -0,0 +1,40 @@
+%default total
+%inline
+%foreign "C:puts,libc"
+%hint
+%hide
+%builtin
+%spec
+%extern
+%macro
+%runElab
+
+----------------------------------------------------
+
+[
+	["pragma", "%default"],
+	["keyword", "total"],
+
+	["pragma", "%inline"],
+
+	["pragma", "%foreign"],
+	["string", ["\"C:puts,libc\""]],
+
+	["pragma", "%hint"],
+
+	["pragma", "%hide"],
+
+	["pragma", "%builtin"],
+
+	["pragma", "%spec"],
+
+	["pragma", "%extern"],
+
+	["pragma", "%macro"],
+
+	["pragma", "%runElab"]
+]
+
+----------------------------------------------------
+
+Checks for %-prefixed pragmas.

tests/languages/idris/string_feature.test

@@ -8,10 +8,10 @@
 ----------------------------------------------------
 
 [
-	["string", "\"\""],
-	["string", "\"fo\\\"o\""],
-	["string", "\"foo \\\r\n  \\ bar\""],
-	["string", "\"foo -- comment \\\r\n  \\ bar\""]
+	["string", ["\"\""]],
+	["string", ["\"fo\\\"o\""]],
+	["string", ["\"foo \\\r\n  \\ bar\""]],
+	["string", ["\"foo -- comment \\\r\n  \\ bar\""]]
 ]
 
 ----------------------------------------------------