Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[code] Preserve original focus when refocusing the panel. #725

Merged
merged 1 commit into from
May 27, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -140,11 +140,14 @@
feature inspired from Isabelle IDE (@ejgallego, #717)
- Have VSCode wait for full LSP client shutdown on server
restart. This fixes some bugs on extension restart (finally!)
(@ejgallgo, #719)
(@ejgallego, #719)
- Center the view if cursor goes out of scope in
`sentenceNext/sentencePrevious` (@ejgallego, #718)
- Switch Flèche range encoding to protocol native, this means UTF-16
for now (Léo Stefanesco, @ejgallego, #624, fixes #620, #621)
- Give `Goals` panel focus back if it has lost it (in case of
multiple panels in the second viewColumn of Vscode) whenever
user navigates proofs (@Alidra @ejgallego, #722, #725)

# coq-lsp 0.1.8.1: Spring fix
-----------------------------
Expand Down
3 changes: 0 additions & 3 deletions editor/code/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,9 +1,6 @@
# coq-lsp 0.1.8: Trick-or-treat
-------------------------------

- Give `Goals` panel focus back if it has lost it (in case of
multiple panels in the second viewColumn of Vscode) whenever
user navigates proofs
- Update VSCode client dependencies, should bring some performance
improvements to goal pretty printing (@ejgallego, #530)
- Update goal display colors for light mode so they are actually
Expand Down
2 changes: 1 addition & 1 deletion editor/code/src/goals.ts
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ export class InfoPanel {
this.panelFactory();
} else {
if (!this.panel.active) {
this.panel.reveal(2, false);
this.panel.reveal(2, true);
}
}
}
Expand Down
Loading