jeans/arduino-ide
jeans/arduino-ide
1
0
Fork 0
mirror of https://github.com/arduino/arduino-ide.git synced 2025-04-19 12:57:17 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix: prevent OutputWidget to gain focus when updated (#2681)

Browse Source
This commit is contained in:
Giacomo Cusinato 2025-04-04 00:51:30 +09:00 committed by GitHub
parent 4d52bb2843
commit e36f393682
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 34 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
arduino-ide-extension/src/browser/theia/core/application-shell.ts
View File

@ -13,6 +13,8 @@ import { MessageService } from '@theia/core/lib/common/message-service';
import { inject, injectable } from '@theia/core/shared/inversify';
import { ApplicationConnectionStatusContribution } from './connection-status-service';
import { ToolbarAwareTabBar } from './tab-bars';
import { find } from '@theia/core/shared/@phosphor/algorithm';
import { OutputWidget } from '@theia/output/lib/browser/output-widget';
@injectable()
export class ApplicationShell extends TheiaApplicationShell {
@ -48,6 +50,38 @@ export class ApplicationShell extends TheiaApplicationShell {
return super.addWidget(widget, { ...options, ref });
}
override doRevealWidget(id: string): Widget | undefined {
let widget = find(this.mainPanel.widgets(), (w) => w.id === id);
if (!widget) {
widget = find(this.bottomPanel.widgets(), (w) => w.id === id);
if (widget) {
this.expandBottomPanel();
}
}
if (widget) {
const tabBar = this.getTabBarFor(widget);
if (tabBar) {
tabBar.currentTitle = widget.title;
}
}
if (!widget) {
widget = this.leftPanelHandler.expand(id);
}
if (!widget) {
widget = this.rightPanelHandler.expand(id);
}
if (widget) {
// Prevent focusing the output widget when is updated
// See https://github.com/arduino/arduino-ide/issues/2679
if (!(widget instanceof OutputWidget)) {
this.windowService.focus();
}
return widget;
} else {
return this.secondaryWindowHandler.revealWidget(id);
}
}
override handleEvent(): boolean {
// NOOP, dragging has been disabled
return false;