mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-11-10 02:48:33 +00:00
Implemented filter and update all for libs/boards.
Closes #177 Closes #1188 Co-authored-by: Francesco Spissu <f.spissu@arduino.cc> Co-authored-by: Per Tillisch <p.tillisch@arduino.cc> Co-authored-by: Akos Kitta <a.kitta@arduino.cc> Signed-off-by: Akos Kitta <a.kitta@arduino.cc>
This commit is contained in:
@@ -0,0 +1,19 @@
|
||||
import { injectable } from '@theia/core/shared/inversify';
|
||||
import { PreferencesEditorWidget as TheiaPreferencesEditorWidget } from '@theia/preferences/lib/browser/views/preference-editor-widget';
|
||||
|
||||
@injectable()
|
||||
export class PreferencesEditorWidget extends TheiaPreferencesEditorWidget {
|
||||
protected override resetScroll(
|
||||
nodeIDToScrollTo?: string,
|
||||
filterWasCleared = false
|
||||
): void {
|
||||
if (this.scrollBar) {
|
||||
// Absent on widget creation
|
||||
this.doResetScroll(nodeIDToScrollTo, filterWasCleared);
|
||||
} else {
|
||||
// NOOP
|
||||
// Unlike Theia, IDE2 does not start multiple tasks to check if the scrollbar is ready to reset it.
|
||||
// If the "scroll reset" request arrived before the existence of the scrollbar, what to reset?
|
||||
}
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user