# HG changeset patch
# User wenzelm
# Date 1762178898 -3600
# Node ID 65f9ca28cebf710d38f74f1218ea3445ba9b0386
# Parent  deb38f8c3ef4aa176017673ef38e6d452a6a6304
unused;

diff -r deb38f8c3ef4 -r 65f9ca28cebf src/Tools/VSCode/extension/src/documentation_panel.ts
--- a/src/Tools/VSCode/extension/src/documentation_panel.ts	Mon Nov 03 15:05:39 2025 +0100
+++ b/src/Tools/VSCode/extension/src/documentation_panel.ts	Mon Nov 03 15:08:18 2025 +0100
@@ -21,7 +21,6 @@
 
   private _view?: WebviewView;
   private _documentation_sections: any[] = [];
-  private _initialized = false;
 
   constructor(
     private readonly _extension_uri: Uri,
@@ -70,8 +69,6 @@
         this._open_document(message.platform_path);
       }
     });
-
-    this._initialized = true;
   }
 
   private _update_webview(): void {
diff -r deb38f8c3ef4 -r 65f9ca28cebf src/Tools/VSCode/extension/src/symbol_panel.ts
--- a/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 15:05:39 2025 +0100
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 15:08:18 2025 +0100
@@ -21,7 +21,6 @@
 
   private _view?: WebviewView
   private _grouped_symbols: { [key: string]: lsp.Symbol_Entry[] } = {}
-  private _initialized = false;
   private _abbrevs: [string, string][] = [];
 
   constructor(
@@ -81,9 +80,6 @@
         this._apply_control_effect(message.action);
       }
     });
-
-
-    this._initialized = true;
   }
 
   private _apply_control_effect(action: string): void {