From 964fb77fa50e88f29ddf82d16d9d15b5ed587327 Mon Sep 17 00:00:00 2001
From: Calixte Denizet <calixte.denizet@gmail.com>
Date: Tue, 19 Jul 2022 23:04:26 +0200
Subject: [PATCH] [Editor] Remove useless and potentially deleted editors

After a deletion, a reference on a deleted editor can still be used
(for example in changing the font size just after having deleted all
editors).
---
 src/display/editor/tools.js | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/src/display/editor/tools.js b/src/display/editor/tools.js
index 7680a5483..f76e147bb 100644
--- a/src/display/editor/tools.js
+++ b/src/display/editor/tools.js
@@ -786,6 +786,7 @@ class AnnotationEditorUIManager {
   delete() {
     let cmd, undo;
     if (this.#isAllSelected) {
+      this.#previousActiveEditor = this.#activeEditor = null;
       const editors = Array.from(this.#allEditors.values());
       cmd = () => {
         for (const editor of editors) {
@@ -807,6 +808,7 @@ class AnnotationEditorUIManager {
         return;
       }
       const editor = this.#activeEditor;
+      this.#previousActiveEditor = this.#activeEditor = null;
       cmd = () => {
         editor.remove();
       };
@@ -834,15 +836,7 @@ class AnnotationEditorUIManager {
   cut() {
     if (this.#activeEditor) {
       this.#clipboardManager.copy(this.#activeEditor);
-      const editor = this.#activeEditor;
-      const cmd = () => {
-        editor.remove();
-      };
-      const undo = () => {
-        this.#addEditorToLayer(editor);
-      };
-
-      this.addCommands({ cmd, undo, mustExec: true });
+      this.delete();
     }
   }