feat: make name of "fetch cache for focused file" command more user-f…

…riendly
leanprover · Oct 29, 2024 · 6358b0c · 6358b0c
1 parent a4eb1ce
commit 6358b0c
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/vscode-lean4/manual/manual.md b/vscode-lean4/manual/manual.md
@@ -611,7 +611,7 @@ The Lean 4 VS Code extension supports the following commands that can be run in
 1. **['Project: Clean Project'](command:lean4.project.clean)**. Removes all build artifacts for the Lean project. If the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it, it will also offer to download and install the current Mathlib build artifact cache after cleaning the project.
 1. **['Project: Update Dependency…'](command:lean4.project.updateDependency)**. Displays a list of all dependencies that can be updated. After selecting a dependency and updating it, if the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it, it will also download and install the current Mathlib build artifact cache. At the end, if the Lean toolchain of the updated project differs from the Lean toolchain of the project, the command will offer to update the Lean toolchain of the project to that of the updated dependency.
 1. **['Project: Fetch Mathlib Build Cache'](command:lean4.project.fetchCache)**. Downloads and installs the current Mathlib build artifact cache if the project is [Mathlib](https://github.com/leanprover-community/mathlib4) or depends on it.
-1. **['Project: Fetch Mathlib Build Cache For Focused File'](command:lean4.project.fetchFileCache)**. Downloads and installs the current Mathlib build artifact for the focused file if the project is [Mathlib](https://github.com/leanprover-community/mathlib4).
+1. **['Project: Fetch Mathlib Build Cache For Current Imports'](command:lean4.project.fetchFileCache)**. Downloads and installs the current Mathlib build artifact for the focused file and all of its imports if the project is [Mathlib](https://github.com/leanprover-community/mathlib4).
 
 <br/>
 

diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
@@ -365,8 +365,8 @@
             {
                 "command": "lean4.project.fetchFileCache",
                 "category": "Lean 4",
-                "title": "Project: Fetch Mathlib Build Cache For Focused File",
-                "description": "Downloads cached Mathlib build artifacts of the focused file to avoid full elaboration"
+                "title": "Project: Fetch Mathlib Build Cache For Current Imports",
+                "description": "Downloads cached Mathlib build artifacts of the focused file and all of its imports to avoid full elaboration"
             }
         ],
         "languages": [

diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts
@@ -33,7 +33,7 @@ export class ProjectOperationProvider implements Disposable {
             commands.registerCommand('lean4.project.clean', () => this.cleanProject()),
             commands.registerCommand('lean4.project.updateDependency', () => this.updateDependency()),
             commands.registerCommand('lean4.project.fetchCache', () => this.fetchMathlibCache()),
-            commands.registerCommand('lean4.project.fetchFileCache', () => this.fetchMathlibCacheForFocusedFile()),
+            commands.registerCommand('lean4.project.fetchFileCache', () => this.fetchMathlibCacheForCurrentImports()),
         )
     }
 
@@ -125,8 +125,8 @@ export class ProjectOperationProvider implements Disposable {
         })
     }
 
-    private async fetchMathlibCacheForFocusedFile() {
-        await this.runOperation('Fetch Mathlib Build Cache For Focused File', async lakeRunner => {
+    private async fetchMathlibCacheForCurrentImports() {
+        await this.runOperation('Fetch Mathlib Build Cache For Current Imports', async lakeRunner => {
             const projectUri = lakeRunner.cwdUri!
 
             if (!window.activeTextEditor || window.activeTextEditor.document.languageId !== 'lean4') {