Skip to content

Commit 86a4fc6

Browse files
Colin Grantjfaltermeier
Colin Grant
authored andcommitted
More flexible editor and editor preview handling
1 parent b9a94e5 commit 86a4fc6

File tree

4 files changed

+85
-65
lines changed

4 files changed

+85
-65
lines changed

packages/core/src/browser/shell/application-shell.ts

Lines changed: 32 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -795,36 +795,13 @@ export class ApplicationShell extends Widget {
795795
*
796796
* Widgets added to the top area are not tracked regarding the _current_ and _active_ states.
797797
*/
798-
async addWidget(widget: Widget, options: Readonly<ApplicationShell.WidgetOptions> = {}): Promise<void> {
798+
async addWidget(widget: Widget, options?: Readonly<ApplicationShell.WidgetOptions>): Promise<void> {
799799
if (!widget.id) {
800800
console.error('Widgets added to the application shell must have a unique id property.');
801801
return;
802802
}
803-
let ref: Widget | undefined = options.ref;
804-
let area: ApplicationShell.Area = options.area || 'main';
805-
if (!ref && (area === 'main' || area === 'bottom')) {
806-
const tabBar = this.getTabBarFor(area);
807-
ref = tabBar && tabBar.currentTitle && tabBar.currentTitle.owner || undefined;
808-
}
809-
// make sure that ref belongs to area
810-
area = ref && this.getAreaFor(ref) || area;
811-
const addOptions: DockPanel.IAddOptions = {};
812-
if (ApplicationShell.isOpenToSideMode(options.mode)) {
813-
const areaPanel = area === 'main' ? this.mainPanel : area === 'bottom' ? this.bottomPanel : undefined;
814-
const sideRef = areaPanel && ref && (options.mode === 'open-to-left' ?
815-
areaPanel.previousTabBarWidget(ref) :
816-
areaPanel.nextTabBarWidget(ref));
817-
if (sideRef) {
818-
addOptions.ref = sideRef;
819-
} else {
820-
addOptions.ref = ref;
821-
addOptions.mode = options.mode === 'open-to-left' ? 'split-left' : 'split-right';
822-
}
823-
} else {
824-
addOptions.ref = ref;
825-
addOptions.mode = options.mode;
826-
}
827-
const sidePanelOptions: SidePanel.WidgetOptions = { rank: options.rank };
803+
const { area, addOptions } = this.getInsertionOptions(options);
804+
const sidePanelOptions: SidePanel.WidgetOptions = { rank: options?.rank };
828805
switch (area) {
829806
case 'main':
830807
this.mainPanel.addWidget(widget, addOptions);
@@ -842,13 +819,41 @@ export class ApplicationShell extends Widget {
842819
this.rightPanelHandler.addWidget(widget, sidePanelOptions);
843820
break;
844821
default:
845-
throw new Error('Unexpected area: ' + options.area);
822+
throw new Error('Unexpected area: ' + options?.area);
846823
}
847824
if (area !== 'top') {
848825
this.track(widget);
849826
}
850827
}
851828

829+
getInsertionOptions(options?: Readonly<ApplicationShell.WidgetOptions>): { area: string; addOptions: DockLayout.IAddOptions; } {
830+
let ref: Widget | undefined = options?.ref;
831+
let area: ApplicationShell.Area = options?.area || 'main';
832+
if (!ref && (area === 'main' || area === 'bottom')) {
833+
const tabBar = this.getTabBarFor(area);
834+
ref = tabBar && tabBar.currentTitle && tabBar.currentTitle.owner || undefined;
835+
}
836+
// make sure that ref belongs to area
837+
area = ref && this.getAreaFor(ref) || area;
838+
const addOptions: DockPanel.IAddOptions = {};
839+
if (ApplicationShell.isOpenToSideMode(options?.mode)) {
840+
const areaPanel = area === 'main' ? this.mainPanel : area === 'bottom' ? this.bottomPanel : undefined;
841+
const sideRef = areaPanel && ref && (options?.mode === 'open-to-left' ?
842+
areaPanel.previousTabBarWidget(ref) :
843+
areaPanel.nextTabBarWidget(ref));
844+
if (sideRef) {
845+
addOptions.ref = sideRef;
846+
} else {
847+
addOptions.ref = ref;
848+
addOptions.mode = options?.mode === 'open-to-left' ? 'split-left' : 'split-right';
849+
}
850+
} else {
851+
addOptions.ref = ref;
852+
addOptions.mode = options?.mode;
853+
}
854+
return { area, addOptions };
855+
}
856+
852857
/**
853858
* The widgets contained in the given shell area.
854859
*/

packages/editor-preview/src/browser/editor-preview-manager.ts

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
import { EditorManager, EditorOpenerOptions, EditorWidget } from '@theia/editor/lib/browser';
1818
import { inject, injectable, postConstruct } from '@theia/core/shared/inversify';
1919
import { EditorPreviewPreferences } from './editor-preview-preferences';
20-
import { DisposableCollection, MaybePromise } from '@theia/core/lib/common';
20+
import { MaybePromise } from '@theia/core/lib/common';
2121
import URI from '@theia/core/lib/common/uri';
2222
import { EditorPreviewWidgetFactory, EditorPreviewOptions } from './editor-preview-widget-factory';
2323
import { EditorPreviewWidget } from './editor-preview-widget';
@@ -30,8 +30,6 @@ export class EditorPreviewManager extends EditorManager {
3030
@inject(EditorPreviewPreferences) protected readonly preferences: EditorPreviewPreferences;
3131
@inject(FrontendApplicationStateService) protected readonly stateService: FrontendApplicationStateService;
3232

33-
protected currentPreview: EditorPreviewWidget | undefined;
34-
protected toDisposeOnPreviewChange = new DisposableCollection();
3533
/**
3634
* Until the layout has been restored, widget state is not reliable, so we ignore creation events.
3735
*/
@@ -44,17 +42,19 @@ export class EditorPreviewManager extends EditorManager {
4442
this.onCreated((widget: EditorPreviewWidget) => {
4543
if (this.layoutIsSet && widget.isPreview) {
4644
const oneTimeDisposable = widget.onDidChangeVisibility(() => {
47-
const { currentPreview } = this;
4845
this.handleNewPreview(widget);
49-
currentPreview?.dispose();
5046
oneTimeDisposable.dispose();
5147
});
5248
}
5349
});
5450

5551
this.preferences.onPreferenceChanged(change => {
5652
if (!change.newValue) {
57-
this.currentPreview?.convertToNonPreview();
53+
this.all.forEach((editor: EditorPreviewWidget) => {
54+
if (editor.isPreview) {
55+
editor.convertToNonPreview();
56+
}
57+
});
5858
};
5959
});
6060

@@ -73,13 +73,8 @@ export class EditorPreviewManager extends EditorManager {
7373
protected override async doOpen(widget: EditorPreviewWidget, options?: EditorOpenerOptions): Promise<void> {
7474
const { preview, widgetOptions = { area: 'main' }, mode = 'activate' } = options ?? {};
7575
if (!widget.isAttached) {
76-
if (preview) {
77-
const insertionOptions = this.currentPreview ? { ref: this.currentPreview } : widgetOptions;
78-
await this.shell.addWidget(widget, insertionOptions);
79-
} else {
80-
this.shell.addWidget(widget, widgetOptions);
81-
}
82-
} else if (!preview && widget === this.currentPreview) {
76+
this.shell.addWidget(widget, widgetOptions);
77+
} else if (!preview && widget.isPreview) {
8378
widget.convertToNonPreview();
8479
}
8580

@@ -90,12 +85,17 @@ export class EditorPreviewManager extends EditorManager {
9085
}
9186
}
9287

93-
protected handleNewPreview(widget: EditorPreviewWidget): void {
94-
this.toDisposeOnPreviewChange.dispose();
95-
this.currentPreview = widget;
96-
this.toDisposeOnPreviewChange.push({ dispose: () => this.currentPreview = undefined });
97-
this.toDisposeOnPreviewChange.push(widget.onDidChangePreviewState(() => this.toDisposeOnPreviewChange.dispose()));
98-
this.toDisposeOnPreviewChange.push(widget.onDidDispose(() => this.toDisposeOnPreviewChange.dispose()));
88+
protected handleNewPreview(newPreviewWidget: EditorPreviewWidget): void {
89+
if (newPreviewWidget.isPreview) {
90+
const tabbar = this.shell.getTabBarFor(newPreviewWidget);
91+
if (tabbar) {
92+
for (const title of tabbar.titles) {
93+
if (title.owner !== newPreviewWidget && title.owner instanceof EditorPreviewWidget && title.owner.isPreview) {
94+
title.owner.dispose();
95+
}
96+
}
97+
}
98+
}
9999
}
100100

101101
protected override tryGetPendingWidget(uri: URI, options?: EditorOpenerOptions): MaybePromise<EditorWidget> | undefined {
@@ -118,8 +118,8 @@ export class EditorPreviewManager extends EditorManager {
118118

119119
protected convertEditorOnDoubleClick(event: Event): void {
120120
const widget = this.shell.findTargetedWidget(event);
121-
if (widget === this.currentPreview) {
122-
this.currentPreview?.convertToNonPreview();
121+
if (widget instanceof EditorPreviewWidget && widget.isPreview) {
122+
widget.convertToNonPreview();
123123
}
124124
}
125125
}

packages/editor/src/browser/editor-manager.ts

Lines changed: 20 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -185,20 +185,28 @@ export class EditorManager extends NavigatableWidgetOpenHandler<EditorWidget> {
185185
return 100;
186186
}
187187

188-
// This override only serves to inform external callers that they can use EditorOpenerOptions.
189188
override open(uri: URI, options?: EditorOpenerOptions): Promise<EditorWidget> {
190-
191-
/* check whether we have a split request without a counter */
192-
if (options && options.counter === undefined && options.widgetOptions?.mode) {
193-
switch (options.widgetOptions.mode) {
194-
case 'split-right':
195-
case 'split-bottom':
196-
case 'split-top':
197-
case 'split-left':
198-
const counter = this.createCounterForUri(uri);
199-
const splitOptions: EditorOpenerOptions = { counter, ...options };
200-
return super.open(uri, splitOptions);
189+
if (options?.counter === undefined) {
190+
const insertionOptions = this.shell.getInsertionOptions(options?.widgetOptions);
191+
// Definitely creating a new tabbar - no widget can match.
192+
if (insertionOptions.addOptions.mode?.startsWith('split')) {
193+
return super.open(uri, { counter: this.createCounterForUri(uri), ...options });
194+
}
195+
// Check the target tabbar for an existing widget.
196+
const tabbar = insertionOptions.addOptions.ref && this.shell.getTabBarFor(insertionOptions.addOptions.ref);
197+
if (tabbar) {
198+
const currentUri = uri.toString();
199+
for (const title of tabbar.titles) {
200+
if (title.owner instanceof EditorWidget) {
201+
const { uri: otherWidgetUri, id } = this.extractIdFromWidget(title.owner);
202+
if (otherWidgetUri === currentUri) {
203+
return super.open(uri, { counter: id, ...options });
204+
}
205+
}
206+
}
201207
}
208+
// Open a new widget.
209+
return super.open(uri, { counter: this.createCounterForUri(uri), ...options });
202210
}
203211

204212
return super.open(uri, options);

packages/plugin-ext/src/main/browser/documents-main.ts

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -251,12 +251,19 @@ export class DocumentsMainImpl implements DocumentsMain, Disposable {
251251
if (viewColumn === undefined || viewColumn === -1) {
252252
/* active group -> skip (default behaviour) */
253253
widgetOptions = undefined;
254-
} else if (viewColumn > 0) {
254+
} else if (viewColumn > 0 && shell.mainAreaTabBars.length > 0) {
255255
const tabBars = shell.mainAreaTabBars;
256-
// convert to zero-based index
257-
const tabBar = tabBars[viewColumn - 1];
258-
if (tabBar && tabBar.currentTitle) {
259-
widgetOptions = { ref: tabBar.currentTitle.owner };
256+
if (viewColumn <= tabBars.length) {
257+
// convert to zero-based index
258+
const tabBar = tabBars[viewColumn - 1];
259+
if (tabBar?.currentTitle) {
260+
widgetOptions = { ref: tabBar.currentTitle.owner };
261+
}
262+
} else {
263+
const tabBar = tabBars[tabBars.length - 1];
264+
if (tabBar?.currentTitle) {
265+
widgetOptions!.ref = tabBar.currentTitle.owner;
266+
}
260267
}
261268
}
262269
return {

0 commit comments

Comments
 (0)