Fix 'try this' in untitled windows

leanprover · May 19, 2022 · c159676 · c159676
1 parent 8d2efce
commit c159676
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;
             }
         }