Skip to content

Commit

Permalink
Fix Vscode extension : Prevent Goals panel to take focus when browsin…
Browse files Browse the repository at this point in the history
…g proofs (#1134)

* vscode: remove debugin message

* vscode: set preserveFocus to true to prevent Goals panel from taking focus each time
  • Loading branch information
Alidra authored Sep 24, 2024
1 parent 82d2d39 commit a83b469
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions editors/vscode/src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -704,9 +704,8 @@ function sendGoalsRequest(position: Position, panel: WebviewPanel, docUri: Uri,
return;
}
// Take focus back if the goal panel lost it.
window.showErrorMessage("Going through Goals");
if(!panel.active) {
panel.reveal(2, false);
panel.reveal(2, true);
}

updateTerminalText(goals.logs);
Expand Down

0 comments on commit a83b469

Please sign in to comment.