149 self.__unsetCalltipsHook(editor) |
149 self.__unsetCalltipsHook(editor) |
150 |
150 |
151 self.__disconnectMouseClickHandler(editor) |
151 self.__disconnectMouseClickHandler(editor) |
152 |
152 |
153 editor.unregisterMouseHoverHelpFunction(self.__jediServer.hoverHelp) |
153 editor.unregisterMouseHoverHelpFunction(self.__jediServer.hoverHelp) |
|
154 self.__jediServer.forgetEditor(editor) |
154 |
155 |
155 with contextlib.suppress(TypeError): |
156 with contextlib.suppress(TypeError): |
156 editor.showMenu.disconnect(self.__editorShowMenu) |
157 editor.showMenu.disconnect(self.__editorShowMenu) |
157 menu = editor.getMenu("Main") |
158 menu = editor.getMenu("Main") |
158 if menu is not None and editor in self.__menuActions: |
159 if menu is not None and editor in self.__menuActions: |