[web] close connection permanently when opening out-of-sync modal (#23148)

* [web] close connection permanently when opening out-of-sync modal

* [web] disable generic forceDisconnected behavior for out-of-sync modal

* [web] hide "disconnected" banner when displaying out of sync modal

GitOrigin-RevId: 133b3e24d94279917298ce7fd5d0a76da2265512
This commit is contained in:
Jakob Ackermann
2025-02-03 09:05:34 +00:00
committed by Copybot
parent cebaebc356
commit 8df7f6772c
6 changed files with 28 additions and 15 deletions
@@ -98,7 +98,7 @@ export const EditorManagerProvider: FC = ({ children }) => {
const { projectId } = useIdeReactContext()
const { reportError, eventEmitter, eventLog } = useIdeReactContext()
const { setOutOfSync } = useEditorContext()
const { socket, disconnect, connectionState } = useConnectionContext()
const { socket, closeConnection, connectionState } = useConnectionContext()
const { view, setView } = useLayoutContext()
const { showGenericMessageModal, genericModalVisible, showOutOfSyncModal } =
useModalsContext()
@@ -580,7 +580,7 @@ export const EditorManagerProvider: FC = ({ children }) => {
// Do not re-join after re-connecting.
document.leaveAndCleanUp()
disconnect()
closeConnection('out-of-sync')
reportError(error, meta)
// Tell the user about the error state.
@@ -605,7 +605,7 @@ export const EditorManagerProvider: FC = ({ children }) => {
}
}
}, [
disconnect,
closeConnection,
docError,
docTooLongErrorShown,
eventEmitter,