# HG changeset patch
# User wenzelm
# Date 1762166465 -3600
# Node ID 53fa51e38c201bad440e85e13b88d2a0c0641913
# Parent  80908b334dc7b4d09eb3c676473cc6da10e5ef2b
clarified names: avoid camel-case;

diff -r 80908b334dc7 -r 53fa51e38c20 src/Tools/VSCode/extension/media/symbols.js
--- a/src/Tools/VSCode/extension/media/symbols.js	Mon Nov 03 11:31:51 2025 +0100
+++ b/src/Tools/VSCode/extension/media/symbols.js	Mon Nov 03 11:41:05 2025 +0100
@@ -1,7 +1,7 @@
 (function () {
   const vscode = acquireVsCodeApi();
   let all_symbols = {};
-  let all_abbrevs_from_thy = [];
+  let all_abbrevs = [];
   let control_sup = "";
   let control_sub = "";
 
@@ -165,16 +165,16 @@
     });
   }
 
-  function render_symbols(grouped_symbols, abbrevs_from_thy) {
+  function render_symbols(grouped_symbols, abbrevs) {
     const container = document.getElementById("symbols-container");
     container.innerHTML = "";
 
     all_symbols = grouped_symbols;
-    all_abbrevs_from_thy = abbrevs_from_thy || [];
+    all_abbrevs = abbrevs || [];
 
     extract_control_symbols(grouped_symbols);
 
-    vscode.setState({ symbols: grouped_symbols, abbrevs_from_Thy: all_abbrevs_from_thy });
+    vscode.setState({ symbols: grouped_symbols, all_abbrevs });
 
     if (!grouped_symbols || Object.keys(grouped_symbols).length === 0) {
       container.innerHTML = "<p>No symbols available.</p>";
@@ -275,7 +275,7 @@
     abbrevs_content.classList.add("tab-content", "hidden");
     abbrevs_content.id = "abbrevs-tab-content";
 
-    all_abbrevs_from_thy
+    all_abbrevs
       .filter(([abbr, symbol]) => symbol && symbol.trim() !== "" && !/^[a-zA-Z0-9 _-]+$/.test(symbol)) 
       .forEach(([abbr, symbol]) => {
         const btn = document.createElement("div");
@@ -339,14 +339,14 @@
 
   window.addEventListener("message", event => {
     if (event.data.command === "update" && event.data.symbols) {
-      render_symbols(event.data.symbols, event.data.abbrevs_from_Thy);
+      render_symbols(event.data.symbols, event.data.abbrevs);
     }
   });
 
   window.onload = function () {
     const state = vscode.getState();
     if (state && state.symbols) {
-      render_symbols(state.symbols, state.abbrevs_from_Thy);
+      render_symbols(state.symbols, state.abbrevs);
     }
   };
 
diff -r 80908b334dc7 -r 53fa51e38c20 src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Mon Nov 03 11:31:51 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Mon Nov 03 11:41:05 2025 +0100
@@ -153,7 +153,7 @@
 
 export interface Symbols_Response {
   symbols: Symbol_Entry [];
-  abbrevs_from_Thy: [string, string][];
+  abbrevs: [string, string][];
 }
 
 export const symbols_request_type =
diff -r 80908b334dc7 -r 53fa51e38c20 src/Tools/VSCode/extension/src/symbol_panel.ts
--- a/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 11:31:51 2025 +0100
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 11:41:05 2025 +0100
@@ -22,7 +22,7 @@
   private _view?: WebviewView
   private _groupedSymbols: { [key: string]: lsp.Symbol_Entry[] } = {}
   private _initialized = false;
-  private _abbrevsFromThy: [string, string][] = [];
+  private _abbrevs: [string, string][] = [];
 
   constructor(
     private readonly _extension_uri: Uri,
@@ -43,7 +43,7 @@
       }
 
       this._groupedSymbols = this._group_symbols(params.symbols);
-      this._abbrevsFromThy = params.abbrevs_from_Thy ?? [];
+      this._abbrevs = params.abbrevs ?? [];
       if (this._view) {
         this._update_webview();
       }
@@ -203,7 +203,7 @@
     this._view.webview.postMessage({
       command: "update",
       symbols: this._groupedSymbols,
-      abbrevs_from_Thy: this._abbrevsFromThy,
+      abbrevs: this._abbrevs,
     });
   }
 
diff -r 80908b334dc7 -r 53fa51e38c20 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Mon Nov 03 11:31:51 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Mon Nov 03 11:41:05 2025 +0100
@@ -732,7 +732,7 @@
       Notification("PIDE/symbols_response",
         JSON.Object(
           "symbols" -> symbols.entries.map(symbol),
-          "abbrevs_from_Thy" -> (for ((a, b) <- abbrevs) yield List(a, b))))
+          "abbrevs" -> (for ((a, b) <- abbrevs) yield List(a, b))))
     }
   }