diff -r 3a99ac054b39 -r 7ae72d1df070 src/eric7/JediInterface/JediServer.py
--- a/src/eric7/JediInterface/JediServer.py Thu Oct 05 10:06:49 2023 +0200
+++ b/src/eric7/JediInterface/JediServer.py Tue Oct 31 09:22:17 2023 +0100
@@ -985,3 +985,16 @@
self.sendJson("closeProject", {}, idString=JediServer.IdProject)
self.stopClient(idString=JediServer.IdProject)
+
+ def forgetEditor(self, editor):
+ """
+ Public method to forget about the given editor.
+
+ @param editor reference to the editor to forget about
+ @type Editor
+ """
+ for uid in self.__editors:
+ if self.__editors[uid] is editor:
+ with contextlib.suppress(KeyError):
+ del self.__editors[uid]
+ break
