From 9c2ab23165431ae7c00b9e3973b5ae732b9bca72 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 22 May 2024 14:08:57 +0200 Subject: [PATCH] vscode: give focus back to Goals panel when navigating proofs Signed-off-by: Abdelghani ALIDRA --- editor/code/src/goals.ts | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts index ff1aec936..eaddbddfd 100644 --- a/editor/code/src/goals.ts +++ b/editor/code/src/goals.ts @@ -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) {