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

Automatically remove editors for deleted files (#894)

Browse Source
This commit is contained in:
Mark Sujew 2022-03-21 10:44:51 +01:00 committed by GitHub
parent f36df02f5d
commit 4de7737d14
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 16 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -20,6 +20,7 @@ import {
FrontendApplication,
FrontendApplicationContribution,
LocalStorageService,
SaveableWidget,
StatusBar,
StatusBarAlignment,
} from '@theia/core/lib/browser';
@ -70,6 +71,7 @@ import { SaveAsSketch } from './contributions/save-as-sketch';
import { SketchbookWidgetContribution } from './widgets/sketchbook/sketchbook-widget-contribution';
import { IDEUpdaterDialog } from './dialogs/ide-updater/ide-updater-dialog';
import { IDEUpdater } from '../common/protocol/ide-updater';
import { FileSystemFrontendContribution } from '@theia/filesystem/lib/browser/filesystem-frontend-contribution';
const INIT_LIBS_AND_PACKAGES = 'initializedLibsAndPackages';
export const SKIP_IDE_VERSION = 'skipIDEVersion';
@ -159,6 +161,9 @@ export class ArduinoFrontendContribution
@inject(LocalStorageService)
protected readonly localStorageService: LocalStorageService;
@inject(FileSystemFrontendContribution)
protected readonly fileSystemFrontendContribution: FileSystemFrontendContribution;
@inject(IDEUpdater)
protected readonly updater: IDEUpdater;
@ -337,6 +342,17 @@ export class ArduinoFrontendContribution
});
app.shell.leftPanelHandler.removeBottomMenu('settings-menu');
this.fileSystemFrontendContribution.onDidChangeEditorFile(e => {
if (e.type === FileChangeType.DELETED) {
const editorWidget = e.editor;
if (SaveableWidget.is(editorWidget)) {
editorWidget.closeWithoutSaving();
} else {
editorWidget.close();
}
}
});
}
onStop(): void {