mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-07-13 22:36:32 +00:00
ATL-312: Fixed output resize issue.
Signed-off-by: Akos Kitta <kittaakos@typefox.io>
This commit is contained in:
parent
af21f07f84
commit
17de5e1a35
@ -115,6 +115,8 @@ import { WorkspaceDeleteHandler } from './theia/workspace/workspace-delete-handl
|
||||
import { TabBarToolbar } from './theia/core/tab-bar-toolbar';
|
||||
import { EditorWidgetFactory as TheiaEditorWidgetFactory } from '@theia/editor/lib/browser/editor-widget-factory';
|
||||
import { EditorWidgetFactory } from './theia/editor/editor-widget-factory';
|
||||
import { OutputWidget as TheiaOutputWidget } from '@theia/output/lib/browser/output-widget';
|
||||
import { OutputWidget } from './theia/output/output-widget';
|
||||
|
||||
const ElementQueries = require('css-element-queries/src/ElementQueries');
|
||||
|
||||
@ -299,6 +301,8 @@ export default new ContainerModule((bind, unbind, isBound, rebind) => {
|
||||
container.bind(TabBarToolbar).toSelf().inSingletonScope();
|
||||
return container.get(TabBarToolbar);
|
||||
});
|
||||
bind(OutputWidget).toSelf().inSingletonScope();
|
||||
rebind(TheiaOutputWidget).toService(OutputWidget);
|
||||
|
||||
// Show a disconnected status bar, when the daemon is not available
|
||||
bind(ApplicationConnectionStatusContribution).toSelf().inSingletonScope();
|
||||
|
@ -0,0 +1,15 @@
|
||||
import { injectable } from 'inversify';
|
||||
import { Message, Widget } from '@theia/core/lib/browser';
|
||||
import { OutputWidget as TheiaOutputWidget } from '@theia/output/lib/browser/output-widget';
|
||||
|
||||
// Patched after https://github.com/eclipse-theia/theia/issues/8361
|
||||
// Remove this module after ATL-222 and the Theia update.
|
||||
@injectable()
|
||||
export class OutputWidget extends TheiaOutputWidget {
|
||||
|
||||
protected onAfterShow(msg: Message): void {
|
||||
super.onAfterShow(msg);
|
||||
this.onResize(Widget.ResizeMessage.UnknownSize);
|
||||
}
|
||||
|
||||
}
|
Loading…
x
Reference in New Issue
Block a user