Skip to content

Commit 1cf6e56

Browse files
fix
1 parent 39c8db8 commit 1cf6e56

File tree

1 file changed

+57
-0
lines changed

1 file changed

+57
-0
lines changed

Diff for: arduino-ide-extension/src/browser/theia/core/application-shell.ts

+57
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ import { MessageService } from '@theia/core/lib/common/message-service';
1313
import { inject, injectable } from '@theia/core/shared/inversify';
1414
import { ApplicationConnectionStatusContribution } from './connection-status-service';
1515
import { ToolbarAwareTabBar } from './tab-bars';
16+
import { find } from '@theia/core/shared/@phosphor/algorithm';
1617

1718
@injectable()
1819
export class ApplicationShell extends TheiaApplicationShell {
@@ -48,6 +49,62 @@ export class ApplicationShell extends TheiaApplicationShell {
4849
return super.addWidget(widget, { ...options, ref });
4950
}
5051

52+
// override doActivateWidget(id: string): Widget | undefined {
53+
// let widget = find(this.mainPanel.widgets(), (w) => w.id === id);
54+
// if (widget) {
55+
// this.mainPanel.activateWidget(widget);
56+
// }
57+
// if (!widget) {
58+
// widget = find(this.bottomPanel.widgets(), (w) => w.id === id);
59+
// if (widget) {
60+
// this.expandBottomPanel();
61+
// this.bottomPanel.activateWidget(widget);
62+
// }
63+
// }
64+
// if (!widget) {
65+
// widget = this.leftPanelHandler.activate(id);
66+
// }
67+
68+
// if (!widget) {
69+
// widget = this.rightPanelHandler.activate(id);
70+
// }
71+
// if (widget) {
72+
// console.log('activate 111!!!', widget);
73+
// this.windowService.focus();
74+
// return widget;
75+
// }
76+
// return this.secondaryWindowHandler.activateWidget(id);
77+
// }
78+
79+
override doRevealWidget(id: string): Widget | undefined {
80+
let widget = find(this.mainPanel.widgets(), (w) => w.id === id);
81+
if (!widget) {
82+
widget = find(this.bottomPanel.widgets(), (w) => w.id === id);
83+
if (widget) {
84+
this.expandBottomPanel();
85+
}
86+
}
87+
if (widget) {
88+
const tabBar = this.getTabBarFor(widget);
89+
if (tabBar) {
90+
tabBar.currentTitle = widget.title;
91+
}
92+
}
93+
if (!widget) {
94+
widget = this.leftPanelHandler.expand(id);
95+
}
96+
if (!widget) {
97+
widget = this.rightPanelHandler.expand(id);
98+
}
99+
if (widget) {
100+
// this.windowService.focus();
101+
console.log('reveal 222!!!', widget);
102+
return widget;
103+
} else {
104+
return this.secondaryWindowHandler.revealWidget(id);
105+
}
106+
}
107+
51108
override handleEvent(): boolean {
52109
// NOOP, dragging has been disabled
53110
return false;

0 commit comments

Comments
 (0)