Mercurial Repositories > eric / file diff

--- a/src/eric7/JediInterface/JediServer.py	Thu Oct 12 17:23:13 2023 +0200
+++ b/src/eric7/JediInterface/JediServer.py	Fri Oct 13 08:30:15 2023 +0200
@@ -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