# HG changeset patch
# User wenzelm
# Date 1762166568 -3600
# Node ID 347281fe2ac83dcefbf234b5cb4b01d8ec51d0e5
# Parent  53fa51e38c201bad440e85e13b88d2a0c0641913
clarified names: avoid camel-case;

diff -r 53fa51e38c20 -r 347281fe2ac8 src/Tools/VSCode/extension/src/symbol_panel.ts
--- a/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 11:41:05 2025 +0100
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 11:42:48 2025 +0100
@@ -20,7 +20,7 @@
   public static readonly view_type = "isabelle-symbols"
 
   private _view?: WebviewView
-  private _groupedSymbols: { [key: string]: lsp.Symbol_Entry[] } = {}
+  private _grouped_symbols: { [key: string]: lsp.Symbol_Entry[] } = {}
   private _initialized = false;
   private _abbrevs: [string, string][] = [];
 
@@ -42,7 +42,7 @@
 
       }
 
-      this._groupedSymbols = this._group_symbols(params.symbols);
+      this._grouped_symbols = this._group_symbols(params.symbols);
       this._abbrevs = params.abbrevs ?? [];
       if (this._view) {
         this._update_webview();
@@ -66,7 +66,7 @@
 
     view.webview.html = this._get_html()
 
-    if (Object.keys(this._groupedSymbols).length > 0) {
+    if (Object.keys(this._grouped_symbols).length > 0) {
       this._update_webview();
     }
 
@@ -96,7 +96,7 @@
 
     if (!selectedText.trim() && !selection.isEmpty) return;
 
-    const control_group = this._groupedSymbols["control"];
+    const control_group = this._grouped_symbols["control"];
     if (!control_group) return;
 
     const control_symbols: { [key: string]: string } = {};
@@ -167,7 +167,7 @@
 
     if (!selectedText.trim() && !selection.isEmpty) return;
 
-    const control_group = this._groupedSymbols["control"];
+    const control_group = this._grouped_symbols["control"];
     if (!control_group) return;
 
 
@@ -202,7 +202,7 @@
   private _update_webview(): void {
     this._view.webview.postMessage({
       command: "update",
-      symbols: this._groupedSymbols,
+      symbols: this._grouped_symbols,
       abbrevs: this._abbrevs,
     });
   }