Mercurial Repositories > eric / file diff

--- 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