Interface TextEditorsExt

interface TextEditorsExt {
    $acceptEditorDiffInformation(
        id: string,
        diffInformation: undefined | TextEditorDiffInformationDto[],
    ): void;
    $acceptEditorPositionData(data: TextEditorPositionData): void;
    $acceptEditorPropertiesChanged(
        id: string,
        props: EditorChangedPropertiesData,
    ): void;
}