diff --git a/package-lock.json b/package-lock.json index adf5279d..e3c7d217 100644 --- a/package-lock.json +++ b/package-lock.json @@ -728,6 +728,7 @@ "version": "8.0.2", "resolved": "https://registry.npmjs.org/@isaacs/cliui/-/cliui-8.0.2.tgz", "integrity": "sha512-O8jcjabXaleOG9DQ0+ARXWZBTfnP4WNAqzuiJK7ll44AmxGKv/J2M4TPjxjY3znBCfvBXFzucm1twdyFybFqEA==", + "dev": true, "license": "ISC", "dependencies": { "string-width": "^5.1.2", @@ -745,6 +746,7 @@ "version": "6.1.0", "resolved": "https://registry.npmjs.org/ansi-regex/-/ansi-regex-6.1.0.tgz", "integrity": "sha512-7HSX4QQb4CspciLpVFwyRe79O3xsIZDDLER21kERQ71oaPodF8jL725AgJMFAYbooIqolJoRLuM81SpeUkpkvA==", + "dev": true, "license": "MIT", "engines": { "node": ">=12" @@ -757,6 +759,7 @@ "version": "6.2.1", "resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-6.2.1.tgz", "integrity": "sha512-bN798gFfQX+viw3R7yrGWRqnrN2oRkEkUjjl4JNn4E8GxxbjtG3FbrEIIY3l8/hrwUwIeCZvi4QuOTP4MErVug==", + "dev": true, "license": "MIT", "engines": { "node": ">=12" @@ -769,12 +772,14 @@ "version": "9.2.2", "resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-9.2.2.tgz", "integrity": "sha512-L18DaJsXSUk2+42pv8mLs5jJT2hqFkFE4j21wOmgbUqsZ2hL72NsUU785g9RXgo3s0ZNgVl42TiHp3ZtOv/Vyg==", + "dev": true, "license": "MIT" }, "node_modules/@isaacs/cliui/node_modules/string-width": { "version": "5.1.2", "resolved": "https://registry.npmjs.org/string-width/-/string-width-5.1.2.tgz", "integrity": "sha512-HnLOCR3vjcY8beoNLtcjZ5/nxn2afmME6lhrDrebokqMap+XbeW8n9TXpPDOqdGK5qcI3oT0GKTW6wC7EMiVqA==", + "dev": true, "license": "MIT", "dependencies": { "eastasianwidth": "^0.2.0", @@ -792,6 +797,7 @@ "version": "7.1.0", "resolved": "https://registry.npmjs.org/strip-ansi/-/strip-ansi-7.1.0.tgz", "integrity": "sha512-iq6eVVI64nQQTRYq2KtEg2d2uU7LElhTJwsH4YzIHZshxlgZms/wIc4VoDQTlG/IvVIrBKG06CrZnp0qv7hkcQ==", + "dev": true, "license": "MIT", "dependencies": { "ansi-regex": "^6.0.1" @@ -807,6 +813,7 @@ "version": "8.1.0", "resolved": "https://registry.npmjs.org/wrap-ansi/-/wrap-ansi-8.1.0.tgz", "integrity": "sha512-si7QWI6zUMq56bESFvagtmzMdGOtoxfR+Sez11Mobfc7tm+VkUckk9bW2UeffTGVUbOksxmSw0AA2gs8g71NCQ==", + "dev": true, "license": "MIT", "dependencies": { "ansi-styles": "^6.1.0", @@ -2593,24 +2600,6 @@ "@types/estree": "*" } }, - "node_modules/@types/glob": { - "version": "8.1.0", - "resolved": "https://registry.npmjs.org/@types/glob/-/glob-8.1.0.tgz", - "integrity": "sha512-IO+MJPVhoqz+28h1qLAcBEH2+xHMK6MTyHJc7MTnnYb6wsoLR29POVGJ7LycmVXIqyy/4/2ShP5sUwTXuOwb/w==", - "dev": true, - "license": "MIT", - "dependencies": { - "@types/minimatch": "^5.1.2", - "@types/node": "*" - } - }, - "node_modules/@types/glob/node_modules/@types/minimatch": { - "version": "5.1.2", - "resolved": "https://registry.npmjs.org/@types/minimatch/-/minimatch-5.1.2.tgz", - "integrity": "sha512-K0VQKziLUWkVKiRVrx4a40iPaxTUefQmjtkQofBkYRcoaaL/8rhwDWww9qWbrgicNOgnpIsMxyNIUM4+n6dUIA==", - "dev": true, - "license": "MIT" - }, "node_modules/@types/hast": { "version": "3.0.4", "resolved": "https://registry.npmjs.org/@types/hast/-/hast-3.0.4.tgz", @@ -4127,6 +4116,7 @@ "version": "5.0.1", "resolved": "https://registry.npmjs.org/ansi-regex/-/ansi-regex-5.0.1.tgz", "integrity": "sha512-quJQXlTSUGL2LH9SUXo8VwsY4soanhgo6LNSm84E1LBcE8s3O0wpdiRzyR9z/ZZJMlMWv37qOOb9pdJlMUEKFQ==", + "dev": true, "license": "MIT", "engines": { "node": ">=8" @@ -4136,6 +4126,7 @@ "version": "4.3.0", "resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz", "integrity": "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg==", + "dev": true, "license": "MIT", "dependencies": { "color-convert": "^2.0.1" @@ -4997,6 +4988,7 @@ "version": "2.0.1", "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz", "integrity": "sha512-RRECPsj7iu/xb5oKYcsFHSppFNnsj/52OVTRKb4zP5onXwVF3zVmmToNcOfGC+CRDpfK/U584fMg38ZHCaElKQ==", + "dev": true, "license": "MIT", "dependencies": { "color-name": "~1.1.4" @@ -5009,6 +5001,7 @@ "version": "1.1.4", "resolved": "https://registry.npmjs.org/color-name/-/color-name-1.1.4.tgz", "integrity": "sha512-dOy+3AuW3a2wNbZHIuMZpTcgjGuLU/uBL/ubcZF9OXbDo8ff4O8yVp5Bf0efS8uEoYo5q4Fx7dY9OgQGXgAsQA==", + "dev": true, "license": "MIT" }, "node_modules/color-support": { @@ -5450,6 +5443,7 @@ "version": "7.0.6", "resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-7.0.6.tgz", "integrity": "sha512-uV2QOWP2nWzsy2aMp8aRibhi9dlzF5Hgh5SHaB9OiTGEyDTiJJyx0uy51QXdyWbtAHNua4XJzUKca3OzKUd3vA==", + "dev": true, "license": "MIT", "dependencies": { "path-key": "^3.1.0", @@ -6046,6 +6040,7 @@ "version": "0.2.0", "resolved": "https://registry.npmjs.org/eastasianwidth/-/eastasianwidth-0.2.0.tgz", "integrity": "sha512-I88TYZWc9XiYHRQ4/3c5rjjfgkjhLyW2luGIheGERbNQ6OY7yTybanSpDXZa8y7VUP9YmDcYa+eyq4ca7iLqWA==", + "dev": true, "license": "MIT" }, "node_modules/ecdsa-sig-formatter": { @@ -6085,6 +6080,7 @@ "version": "8.0.0", "resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-8.0.0.tgz", "integrity": "sha512-MSjYzcWNOA0ewAHpz0MxpYFvwg6yjy1NG3xteoqz644VCo/RPgnr1/GGt+ic3iJTzQ8Eu3TdM14SawnVUmGE6A==", + "dev": true, "license": "MIT" }, "node_modules/encoding": { @@ -6902,6 +6898,7 @@ "version": "3.3.0", "resolved": "https://registry.npmjs.org/foreground-child/-/foreground-child-3.3.0.tgz", "integrity": "sha512-Ld2g8rrAyMYFXBhEqMz8ZAHBi4J4uS1i/CxGMDnjyFWddMXLVcDp051DZfu+t7+ab7Wv6SMqpWmyFIj5UbfFvg==", + "dev": true, "license": "ISC", "dependencies": { "cross-spawn": "^7.0.0", @@ -6918,6 +6915,7 @@ "version": "4.1.0", "resolved": "https://registry.npmjs.org/signal-exit/-/signal-exit-4.1.0.tgz", "integrity": "sha512-bzyZ1e88w9O1iNJbKnOlvYTrWPDl46O1bG0D3XInv+9tkPrxrN8jUUTiFlDkkmKWgn1M6CfIA13SuGqOa9Korw==", + "dev": true, "license": "ISC", "engines": { "node": ">=14" @@ -8417,6 +8415,7 @@ "version": "2.0.0", "resolved": "https://registry.npmjs.org/isexe/-/isexe-2.0.0.tgz", "integrity": "sha512-RHxMLp9lnKHGHRng9QFhRCMbYAcVpn69smSGcq3f36xjgVVWThj4qqLbTLlq7Ssj8B+fIQ1EuCEGI2lKsyQeIw==", + "dev": true, "license": "ISC" }, "node_modules/isobject": { @@ -11199,6 +11198,7 @@ "version": "7.1.2", "resolved": "https://registry.npmjs.org/minipass/-/minipass-7.1.2.tgz", "integrity": "sha512-qOOzS1cBTWYF4BH8fVePDBOO9iptMnGUEZwNc/cMWnTV2nVLZ7VoNWEPHkYczZA0pdoA7dl6e7FL659nX9S2aw==", + "dev": true, "license": "ISC", "engines": { "node": ">=16 || 14 >=14.17" @@ -12608,6 +12608,7 @@ "version": "1.0.1", "resolved": "https://registry.npmjs.org/package-json-from-dist/-/package-json-from-dist-1.0.1.tgz", "integrity": "sha512-UEZIS3/by4OC8vL3P2dTXRETpebLI2NiI5vIrjaD/5UtrkFX/tNbwjTSRAGC/+7CAo2pIcBaRgWmcBBHcsaCIw==", + "dev": true, "license": "BlueOak-1.0.0" }, "node_modules/pacote": { @@ -12842,6 +12843,7 @@ "version": "3.1.1", "resolved": "https://registry.npmjs.org/path-key/-/path-key-3.1.1.tgz", "integrity": "sha512-ojmeN0qd+y0jszEtoY48r0Peq5dwMEkIlCOu6Q5f41lfkswXuKtYrhgoTpLnyIcHm24Uhqx+5Tqm2InSwLhE6Q==", + "dev": true, "license": "MIT", "engines": { "node": ">=8" @@ -14440,6 +14442,7 @@ "version": "2.0.0", "resolved": "https://registry.npmjs.org/shebang-command/-/shebang-command-2.0.0.tgz", "integrity": "sha512-kHxr2zZpYtdmrN1qDjrrX/Z1rR1kG8Dx+gkpK1G4eXmvXswmcE1hTWBWYUzlraYw1/yZp6YuDY77YtvbN0dmDA==", + "dev": true, "license": "MIT", "dependencies": { "shebang-regex": "^3.0.0" @@ -14452,6 +14455,7 @@ "version": "3.0.0", "resolved": "https://registry.npmjs.org/shebang-regex/-/shebang-regex-3.0.0.tgz", "integrity": "sha512-7++dFhtcx3353uBaq8DDR4NuxBetBzC7ZQOhmTQInHEd6bSrXdiEyzCvG07Z44UYdLShWUyXt5M/yhz8ekcb1A==", + "dev": true, "license": "MIT", "engines": { "node": ">=8" @@ -14935,6 +14939,7 @@ "version": "4.2.3", "resolved": "https://registry.npmjs.org/string-width/-/string-width-4.2.3.tgz", "integrity": "sha512-wKyQRQpjJ0sIp62ErSZdGsjMJWsap5oRNihHhu6G7JVO/9jIB6UyevL+tXuOqrng8j/cxKTWyWUwvSTriiZz/g==", + "dev": true, "license": "MIT", "dependencies": { "emoji-regex": "^8.0.0", @@ -14950,6 +14955,7 @@ "version": "4.2.3", "resolved": "https://registry.npmjs.org/string-width/-/string-width-4.2.3.tgz", "integrity": "sha512-wKyQRQpjJ0sIp62ErSZdGsjMJWsap5oRNihHhu6G7JVO/9jIB6UyevL+tXuOqrng8j/cxKTWyWUwvSTriiZz/g==", + "dev": true, "license": "MIT", "dependencies": { "emoji-regex": "^8.0.0", @@ -14964,6 +14970,7 @@ "version": "3.0.0", "resolved": "https://registry.npmjs.org/is-fullwidth-code-point/-/is-fullwidth-code-point-3.0.0.tgz", "integrity": "sha512-zymm5+u+sCsSWyD9qNaejV3DFvhCKclKdizYaJUuHA83RLjb7nSuGnddCHGv0hk+KY7BMAlsWeK4Ueg6EV6XQg==", + "dev": true, "license": "MIT", "engines": { "node": ">=8" @@ -14973,6 +14980,7 @@ "version": "3.0.0", "resolved": "https://registry.npmjs.org/is-fullwidth-code-point/-/is-fullwidth-code-point-3.0.0.tgz", "integrity": "sha512-zymm5+u+sCsSWyD9qNaejV3DFvhCKclKdizYaJUuHA83RLjb7nSuGnddCHGv0hk+KY7BMAlsWeK4Ueg6EV6XQg==", + "dev": true, "license": "MIT", "engines": { "node": ">=8" @@ -14997,6 +15005,7 @@ "version": "6.0.1", "resolved": "https://registry.npmjs.org/strip-ansi/-/strip-ansi-6.0.1.tgz", "integrity": "sha512-Y38VPSHcqkFrCpFnQ9vuSXmquuv5oXOKpGeT6aGrr3o3Gc9AlVa6JBfUSOCnbxGGZF+/0ooI7KrPuUSztUdU5A==", + "dev": true, "license": "MIT", "dependencies": { "ansi-regex": "^5.0.1" @@ -15010,6 +15019,7 @@ "version": "6.0.1", "resolved": "https://registry.npmjs.org/strip-ansi/-/strip-ansi-6.0.1.tgz", "integrity": "sha512-Y38VPSHcqkFrCpFnQ9vuSXmquuv5oXOKpGeT6aGrr3o3Gc9AlVa6JBfUSOCnbxGGZF+/0ooI7KrPuUSztUdU5A==", + "dev": true, "license": "MIT", "dependencies": { "ansi-regex": "^5.0.1" @@ -16426,6 +16436,7 @@ "version": "2.0.2", "resolved": "https://registry.npmjs.org/which/-/which-2.0.2.tgz", "integrity": "sha512-BLI3Tl1TW3Pvl70l3yq3Y64i+awpwXqsGBYWkkqMtnbXgrMD+yj7rhW0kuEDxzJaYXGjEW5ogapKNMEKNMjibA==", + "dev": true, "license": "ISC", "dependencies": { "isexe": "^2.0.0" @@ -16505,6 +16516,7 @@ "version": "7.0.0", "resolved": "https://registry.npmjs.org/wrap-ansi/-/wrap-ansi-7.0.0.tgz", "integrity": "sha512-YVGIj2kamLSTxw6NsZjoBxfSwsn0ycdesmc4p+Q21c5zPuZ1pl+NfxVdxPtdHvmNVOQ6XSYG4AUtyt/Fi7D16Q==", + "dev": true, "license": "MIT", "dependencies": { "ansi-styles": "^4.0.0", @@ -16891,7 +16903,7 @@ }, "vscode-lean4": { "name": "lean4", - "version": "0.0.188", + "version": "0.0.189", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.8.0", @@ -16900,7 +16912,6 @@ "@leanprover/unicode-input-component": "~0.1.0", "@vscode-elements/elements": "^1.7.1", "@vscode/codicons": "^0.0.36", - "glob": "^11.0.1", "markdown-it": "^14.1.0", "markdown-it-anchor": "^9.0.1", "semver": "^7.6.0", @@ -16908,7 +16919,6 @@ "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", @@ -16919,6 +16929,7 @@ "@vscode/vsce": "^2.21.1", "concurrently": "^8.2.2", "copy-webpack-plugin": "^12.0.2", + "glob": "^10.4.5", "mocha": "^10.3.0", "ovsx": "^0.9.1", "source-map-loader": "^5.0.0", @@ -16948,6 +16959,7 @@ "version": "11.0.1", "resolved": "https://registry.npmjs.org/glob/-/glob-11.0.1.tgz", "integrity": "sha512-zrQDm8XPnYEKawJScsnM0QzobJxlT/kHOOlRTio8IH/GrmxRE5fjllkzdaHclIuNjUQTJYH2xHNIGfdpJkDJUw==", + "dev": true, "dependencies": { "foreground-child": "^3.1.0", "jackspeak": "^4.0.1", @@ -16970,6 +16982,7 @@ "version": "4.0.2", "resolved": "https://registry.npmjs.org/jackspeak/-/jackspeak-4.0.2.tgz", "integrity": "sha512-bZsjR/iRjl1Nk1UkjGpAzLNfQtzuijhn2g+pbZb98HQ1Gk8vM9hfbxeMBP+M2/UUdwj0RqGG3mlvk2MsAqwvEw==", + "dev": true, "dependencies": { "@isaacs/cliui": "^8.0.2" }, @@ -16984,6 +16997,7 @@ "version": "11.0.2", "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-11.0.2.tgz", "integrity": "sha512-123qHRfJBmo2jXDbo/a5YOQrJoHF/GNQTLzQ5+IdK5pWpceK17yRc6ozlWd25FxvGKQbIUs91fDFkXmDHTKcyA==", + "dev": true, "engines": { "node": "20 || >=22" } @@ -16992,6 +17006,7 @@ "version": "10.0.1", "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-10.0.1.tgz", "integrity": "sha512-ethXTt3SGGR+95gudmqJ1eNhRO7eGEGIgYA9vnPatK4/etz2MEVDno5GMCibdMTuBMyElzIlgxMna3K94XDIDQ==", + "dev": true, "dependencies": { "brace-expansion": "^2.0.1" }, @@ -17006,6 +17021,7 @@ "version": "2.0.0", "resolved": "https://registry.npmjs.org/path-scurry/-/path-scurry-2.0.0.tgz", "integrity": "sha512-ypGJsmGtdXUOeM5u93TyeIEfEhM6s+ljAhrk5vAvSx8uyY/02OvrZnA0YNGUrPXfpJMgI1ODd3nwz8Npx4O4cg==", + "dev": true, "dependencies": { "lru-cache": "^11.0.0", "minipass": "^7.1.2" diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index f1f84fa6..647bad43 100644 --- 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 index 90757bf2..61aa81dc 100644 --- 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),