Skip to content

Commit

Permalink
vscode: give focus back to Goals panel when navigating proofs
Browse files Browse the repository at this point in the history
Signed-off-by: Abdelghani ALIDRA <[email protected]>
  • Loading branch information
Alidra committed May 23, 2024
1 parent 5d1a523 commit 9c2ab23
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions editor/code/src/goals.ts
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,10 @@ export class InfoPanel {
ensurePanel() {
if (!this.panel) {
this.panelFactory();
} else {
if (!this.panel.active) {
this.panel.reveal(2, false);
}
}
}
postMessage({ method, params }: CoqMessagePayload) {
Expand Down

0 comments on commit 9c2ab23

Please sign in to comment.