mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-11-17 06:09:28 +00:00
Update Theia, CLI and LS (#610)
* Update Theia to 1.19.0 * update CLI to 0.20.0-rc3 * Add language selector to settings * updated language server and vscode-arduino-tools * update Language Server flags * get cli port from config * force native menu on windows * pinned Language Server to rc2 * fix search icon * update CLI version
This commit is contained in:
@@ -0,0 +1,19 @@
|
||||
import { ViewContainer } from '@theia/core/lib/browser/view-container';
|
||||
import { injectable } from '@theia/core/shared/inversify';
|
||||
|
||||
import {
|
||||
SearchInWorkspaceFactory as TheiaSearchInWorkspaceFactory,
|
||||
SEARCH_VIEW_CONTAINER_TITLE_OPTIONS,
|
||||
} from '@theia/search-in-workspace/lib/browser/search-in-workspace-factory';
|
||||
|
||||
@injectable()
|
||||
export class SearchInWorkspaceFactory extends TheiaSearchInWorkspaceFactory {
|
||||
async createWidget(): Promise<ViewContainer> {
|
||||
const viewContainer = await super.createWidget();
|
||||
viewContainer.setTitleOptions({
|
||||
...SEARCH_VIEW_CONTAINER_TITLE_OPTIONS,
|
||||
iconClass: 'fa fa-arduino-search',
|
||||
});
|
||||
return viewContainer;
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user