tuned names: avoid camel-case;
authorwenzelm
Sun, 02 Nov 2025 23:59:23 +0100
changeset 83466 4e3eae17917f
parent 83465 4023a9c7070f
child 83467 974a67c6cc31
tuned names: avoid camel-case;
src/Tools/VSCode/extension/media/symbols.js
src/Tools/VSCode/extension/src/symbol_panel.ts
--- a/src/Tools/VSCode/extension/media/symbols.js	Sun Nov 02 23:56:01 2025 +0100
+++ b/src/Tools/VSCode/extension/media/symbols.js	Sun Nov 02 23:59:23 2025 +0100
@@ -88,7 +88,7 @@
         button.setAttribute("data-tooltip", `${symbol.symbol}\nAbbreviations: ${symbol.abbrevs.join(", ")}`);
 
         button.addEventListener("click", () => {
-          vscode.postMessage({ command: "insertSymbol", symbol: decoded_symbol });
+          vscode.postMessage({ command: "insert_symbol", symbol: decoded_symbol });
         });
 
         results_container.appendChild(button);
@@ -213,7 +213,7 @@
         reset_button.textContent = "Reset";
 
         reset_button.addEventListener("click", () => {
-          vscode.postMessage({ command: "resetControlSymbols" });
+          vscode.postMessage({ command: "reset_control_symbols" });
         });
         group_content.appendChild(reset_button);
 
@@ -227,7 +227,7 @@
             button.textContent = decoded_symbol;
             button.title = action.charAt(0).toUpperCase() + action.slice(1);
             button.addEventListener("click", () => {
-              vscode.postMessage({ command: "applyControl", action: action });
+              vscode.postMessage({ command: "apply_control", action: action });
             });
             group_content.appendChild(button);
           }
@@ -251,7 +251,7 @@
         button.setAttribute("data-tooltip", `${symbol.symbol}\nAbbreviations: ${symbol.abbrevs.join(", ")}`);
 
         button.addEventListener("click", () => {
-          vscode.postMessage({ command: "insertSymbol", symbol: decoded_symbol });
+          vscode.postMessage({ command: "insert_symbol", symbol: decoded_symbol });
         });
 
         group_content.appendChild(button);
@@ -283,7 +283,7 @@
         btn.innerHTML = render_with_effects(symbol); 
         btn.title = abbr;
         btn.addEventListener("click", () => {
-          vscode.postMessage({ command: "insertSymbol", symbol: convert_symbol_with_effects(sanitize_symbol_for_insert(symbol)) });
+          vscode.postMessage({ command: "insert_symbol", symbol: convert_symbol_with_effects(sanitize_symbol_for_insert(symbol)) });
         });
 
         abbrevs_content.appendChild(btn);
--- a/src/Tools/VSCode/extension/src/symbol_panel.ts	Sun Nov 02 23:56:01 2025 +0100
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts	Sun Nov 02 23:59:23 2025 +0100
@@ -71,13 +71,13 @@
     }
 
     this._view.webview.onDidReceiveMessage(message => {
-      if (message.command === "insertSymbol") {
+      if (message.command === "insert_symbol") {
         this._insert_symbol(message.symbol);
       }
-      else if (message.command === "resetControlSymbols") {
+      else if (message.command === "reset_control_symbols") {
         this._reset_control_symbols();
       }
-      else if (message.command === "applyControl") {
+      else if (message.command === "apply_control") {
         this._apply_control_effect(message.action);
       }
     });