diff -r dcaf9447c083 -r b284ff764c80 src/Tools/VSCode/extension/media/symbols.js
--- a/src/Tools/VSCode/extension/media/symbols.js	Mon Nov 03 17:09:55 2025 +0100
+++ b/src/Tools/VSCode/extension/media/symbols.js	Mon Nov 03 17:17:53 2025 +0100
@@ -5,6 +5,14 @@
   let control_sup = "";
   let control_sub = "";
 
+  function symbol_tooltip(symbol) {
+    const res = [symbol.symbol]
+    for (const a of symbol.abbrevs) {
+      res.push(`\nabbrev: ${a}`);
+    }
+    return res.join("")
+  }
+
   function create_search_field() {
     const search_container = document.createElement("div");
     search_container.classList.add("search-container");
@@ -50,7 +58,7 @@
         const button = document.createElement("div");
         button.classList.add("symbol-button");
         button.textContent = symbol.decoded;
-        button.setAttribute("data-tooltip", `${symbol.symbol}\nAbbreviations: ${symbol.abbrevs.join(", ")}`);
+        button.setAttribute("data-tooltip", symbol_tooltip(symbol));
         button.addEventListener("click", () => {
           vscode.postMessage({ command: "insert_symbol", symbol: symbol.decoded });
         });
@@ -236,8 +244,7 @@
           button.classList.add("symbol-button");
         }
         button.textContent = symbol.decoded;
-        button.setAttribute("data-tooltip", `${symbol.symbol}\nAbbreviations: ${symbol.abbrevs.join(", ")}`);
-
+        button.setAttribute("data-tooltip", symbol_tooltip(symbol));
         button.addEventListener("click", () => {
           vscode.postMessage({ command: "insert_symbol", symbol: symbol.decoded });
         });