chore: use lean4 scope for lean-markdown (leanprover#361)

mhuisi · Nov 26, 2023 · 207c0f1 · 207c0f1
1 parent 2fd18c6
commit 207c0f1
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 10 deletions.
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
@@ -380,10 +380,10 @@
 				"configuration": "./language-configuration.json"
 			},
 			{
-				"id": "leanmarkdown",
+				"id": "lean4markdown",
 				"aliases": [],
 				"extensions": [
-					".leanmarkdown"
+					".lean4markdown"
 				],
 				"configuration": "./language-configuration.json"
 			}
@@ -395,9 +395,9 @@
 				"path": "./syntaxes/lean4.json"
 			},
 			{
-				"language": "leanmarkdown",
-				"scopeName": "source.lean.markdown",
-				"path": "./syntaxes/lean-markdown.json"
+				"language": "lean4markdown",
+				"scopeName": "source.lean4.markdown",
+				"path": "./syntaxes/lean4-markdown.json"
 			},
 			{
 				"scopeName": "markdown.lean4.codeblock",

diff --git a/vscode-lean4/syntaxes/lean-markdown.json → vscode-lean4/syntaxes/lean4-markdown.json b/vscode-lean4/syntaxes/lean-markdown.json → vscode-lean4/syntaxes/lean4-markdown.json
@@ -5,7 +5,7 @@
 	],
 	"version": "https://github.com/microsoft/vscode/blob/df3ae4adefbb780f5f686e58ac6a8d305a8c86dc/extensions/markdown-basics/syntaxes/markdown.tmLanguage.json",
 	"name": "Markdown",
-	"scopeName": "source.lean.markdown",
+	"scopeName": "source.lean4.markdown",
 	"patterns": [
 		{
 			"include": "#frontMatter"

diff --git a/vscode-lean4/syntaxes/lean4.json b/vscode-lean4/syntaxes/lean4.json
@@ -62,27 +62,27 @@
       "begin": "--", "end": "$",
       "name": "comment.line.double-dash.lean4",
       "patterns": [
-        { "include": "source.lean.markdown" }
+        { "include": "source.lean4.markdown" }
       ]
     },
     "docComment": {
       "begin": "/--", "end": "-/", "name": "comment.block.documentation.lean4",
       "patterns": [
-        { "include": "source.lean.markdown" },
+        { "include": "source.lean4.markdown" },
         { "include": "#blockComment" }
       ]
     },
     "modDocComment": {
       "begin": "/-!", "end": "-/", "name": "comment.block.documentation.lean4",
       "patterns": [
-        { "include": "source.lean.markdown" },
+        { "include": "source.lean4.markdown" },
         { "include": "#blockComment" }
       ]
     },
     "blockComment": {
       "begin": "/-", "end": "-/", "name": "comment.block.lean4",
       "patterns": [
-        { "include": "source.lean.markdown" },
+        { "include": "source.lean4.markdown" },
         { "include": "#blockComment" }
       ]
     },