--- 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);
}
});