Merge pull request #303 from eric-wieser/fix-try-this

Fix 'try this' in untitled windows
leanprover · May 19, 2022 · 27c15af · 27c15af
2 parents 8d2efce + c159676
commit 27c15af
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/tacticsuggestions.ts b/src/tacticsuggestions.ts
@@ -42,7 +42,8 @@ export class TacticSuggestions implements Disposable, CodeActionProvider {
 
     private findTextEditor(fileName: string) {
         for (const textEditor of window.visibleTextEditors) {
-            if (textEditor.document.uri.toString() === Uri.file(fileName).toString()) {
+            // note we cannot compare URIs as the `Message` type doesn't contain them
+            if (textEditor.document.fileName === fileName) {
                 return textEditor;
             }
         }