jeans/arduino-ide
jeans/arduino-ide
1
0
Fork 0
mirror of https://github.com/arduino/arduino-ide.git synced 2025-07-08 11:56:36 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fix editor tabs order (#612)

Browse Source
This commit is contained in:
Francesco Stasi 2021-11-23 12:16:56 +01:00 committed by GitHub
parent 13734a642c
commit 9863dc2f90
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 9 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
arduino-ide-extension/src/browser/arduino-frontend-contribution.tsx
View File

@ -508,7 +508,6 @@ export class ArduinoFrontendContribution
for (const uri of [mainFileUri, ...rootFolderFileUris]) { for (const uri of [mainFileUri, ...rootFolderFileUris]) {
await this.ensureOpened(uri); await this.ensureOpened(uri);
} }
await this.ensureOpened(mainFileUri, true);
if (mainFileUri.endsWith('.pde')) { if (mainFileUri.endsWith('.pde')) {
const message = nls.localize( const message = nls.localize(
'arduino/common/oldFormat', 'arduino/common/oldFormat',

13
arduino-ide-extension/src/browser/theia/core/shell-layout-restorer.ts
View File

@ -35,13 +35,18 @@ export class ShellLayoutRestorer extends TheiaShellLayoutRestorer {
const layoutData = await this.inflate(serializedLayoutData); const layoutData = await this.inflate(serializedLayoutData);
// workaround to remove duplicated tabs // workaround to remove duplicated tabs
const filesUri: string[] = [];
if ((layoutData as any)?.mainPanel?.main?.widgets) { if ((layoutData as any)?.mainPanel?.main?.widgets) {
(layoutData as any).mainPanel.main.widgets = ( (layoutData as any).mainPanel.main.widgets = (
layoutData as any layoutData as any
).mainPanel.main.widgets.filter( ).mainPanel.main.widgets.filter((widget: any) => {
(widget: any) => const uri = widget.getResourceUri().toString();
widget.constructionOptions.factoryId !== 'code-editor-opener' if (filesUri.includes(uri)) {
); return false;
}
filesUri.push(uri);
return true;
});
} }
await app.shell.setLayoutData(layoutData); await app.shell.setLayoutData(layoutData);