fix: curly bracket glob escape (#569)

leanprover · Jan 13, 2025 · 8663c3b · 8663c3b
1 parent dbd82c9
commit 8663c3b
Show file tree

Hide file tree

Showing 3 changed files with 42 additions and 27 deletions.
diff --git a/package-lock.json b/package-lock.json
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
@@ -1091,11 +1091,9 @@
         "markdown-it-anchor": "^9.0.1",
         "semver": "^7.6.0",
         "vscode-languageclient": "^8.0.2",
-        "zod": "^3.22.4",
-        "glob": "^11.0.1"
+        "zod": "^3.22.4"
     },
     "devDependencies": {
-        "@types/glob": "^8.1.0",
         "@types/markdown-it": "^14.1.1",
         "@types/mocha": "^10.0.6",
         "@types/node": "^20.12.12",
@@ -1112,7 +1110,8 @@
         "ts-loader": "^9.5.1",
         "typescript": "^5.4.5",
         "webpack": "^5.90.3",
-        "webpack-cli": "^5.1.4"
+        "webpack-cli": "^5.1.4",
+        "glob": "^10.4.5"
     },
     "icon": "images/lean_logo.png",
     "license": "Apache-2.0",

diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts
@@ -1,4 +1,3 @@
-import * as glob from 'glob'
 import {
     DiagnosticCollection,
     Disposable,
@@ -548,7 +547,8 @@ export class LeanClient implements Disposable {
         let workspaceFolder: WorkspaceFolder | undefined
         documentSelector.scheme = this.folderUri.scheme
         if (this.folderUri.scheme === 'file') {
-            documentSelector.pattern = `${glob.escape(this.folderUri.fsPath, { windowsPathsNoEscape: true })}/**/*`
+            const escapedPath = this.folderUri.fsPath.replace(/[?*()[\]{}]/g, '[$&]')
+            documentSelector.pattern = `${escapedPath}/**/*`
             workspaceFolder = {
                 uri: this.folderUri.asUri(),
                 name: path.basename(this.folderUri.fsPath),