# HG changeset patch
# User wenzelm
# Date 1762184274 -3600
# Node ID 499cbd3f6cee3c9d77b5d08c5db87847ab7b27a2
# Parent  447b52014c0eeadfd15e7cd2ac962d0f1f818243
misc tuning;

diff -r 447b52014c0e -r 499cbd3f6cee src/Tools/VSCode/extension/src/symbol_panel.ts
--- a/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 16:31:58 2025 +0100
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 16:37:54 2025 +0100
@@ -1,4 +1,5 @@
 /*  Author:     Diana Korchmar, LMU Muenchen
+    Author:     Makarius
 
 Isabelle symbols panel as web view.
 */
@@ -36,15 +37,12 @@
 
   setup(language_client: LanguageClient) {
     language_client.onNotification(lsp.symbols_response_type, params => {
-      if (!params?.symbols || !Array.isArray(params.symbols)) {
-        return;
-
-      }
-
-      this._grouped_symbols = this._group_symbols(params.symbols);
-      this._abbrevs = params.abbrevs ?? [];
-      if (this._view) {
-        this._update_webview();
+      if (params?.symbols && Array.isArray(params.symbols)) {
+        this._grouped_symbols = this._group_symbols(params.symbols);
+        this._abbrevs = params.abbrevs ?? [];
+        if (this._view) {
+          this._update_webview();
+        }
       }
     });
   }
@@ -206,15 +204,13 @@
   private _group_symbols(symbols: lsp.Symbol_Entry[]): { [key: string]: lsp.Symbol_Entry[] } {
     const grouped_symbols: { [key: string]: lsp.Symbol_Entry[] } = {};
     for (const symbol of symbols) {
-      if (!symbol.groups || !Array.isArray(symbol.groups)) {
-        return;
-      }
-
-      for (const group of symbol.groups) {
-        if (!grouped_symbols[group]) {
-          grouped_symbols[group] = [];
+      if (symbol.groups && Array.isArray(symbol.groups)) {
+        for (const group of symbol.groups) {
+          if (!grouped_symbols[group]) {
+            grouped_symbols[group] = [];
+          }
+          grouped_symbols[group].push(symbol);
         }
-        grouped_symbols[group].push(symbol);
       }
     }
     return grouped_symbols;