feat: syntactic string interpolation highlighting (#404)

Co-authored-by: Trebor-Huang <[email protected]>
leanprover · Mar 12, 2024 · 5bba180 · 5bba180
1 parent 212cbd4
commit 5bba180
Showing 1 changed file with 17 additions and 0 deletions.
diff --git a/vscode-lean4/syntaxes/lean4.json b/vscode-lean4/syntaxes/lean4.json
@@ -35,6 +35,23 @@
       "name": "keyword.other.lean4"
     },
     { "begin": "«", "end": "»", "contentName": "entity.name.lean4" },
+    {
+      "begin": "(s!)\"", "end": "\"",
+      "name": "string.interpolated.lean4",
+      "beginCaptures": {
+        "1": { "name": "keyword.other.lean4" }
+      },
+      "patterns": [
+        {
+          "begin": "(\\{)", "end": "(\\})",
+          "beginCaptures": { "1": { "name": "keyword.other.lean4" } },
+          "endCaptures": { "1": { "name": "keyword.other.lean4" } },
+          "patterns": [ {"include": "$self"} ] },
+        { "match": "\\\\[\\\\\"ntr']", "name": "constant.character.escape.lean4" },
+        { "match": "\\\\x[0-9A-Fa-f][0-9A-Fa-f]", "name": "constant.character.escape.lean4" },
+        { "match": "\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]", "name": "constant.character.escape.lean4" }
+      ]
+    },
     {
       "begin": "\"", "end": "\"",
       "name": "string.quoted.double.lean4",