# HG changeset patch
# User wenzelm
# Date 1762183918 -3600
# Node ID 447b52014c0eeadfd15e7cd2ac962d0f1f818243
# Parent  26e0aafd26ea61b701d42937f6c6a1d486b118d8
clarified names;

diff -r 26e0aafd26ea -r 447b52014c0e src/Tools/VSCode/extension/media/symbols.js
--- a/src/Tools/VSCode/extension/media/symbols.js	Mon Nov 03 15:18:58 2025 +0100
+++ b/src/Tools/VSCode/extension/media/symbols.js	Mon Nov 03 16:31:58 2025 +0100
@@ -174,10 +174,7 @@
         const reset_button = document.createElement("button");
         reset_button.classList.add("reset-button");
         reset_button.textContent = "Reset";
-
-        reset_button.addEventListener("click", () => {
-          vscode.postMessage({ command: "reset_control_symbols" });
-        });
+        reset_button.addEventListener("click", () => vscode.postMessage({ command: "reset_control" }));
         group_content.appendChild(reset_button);
 
         const control_buttons = ["sup", "sub", "bold"];
diff -r 26e0aafd26ea -r 447b52014c0e src/Tools/VSCode/extension/src/symbol_panel.ts
--- a/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 15:18:58 2025 +0100
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts	Mon Nov 03 16:31:58 2025 +0100
@@ -73,16 +73,16 @@
       if (message.command === "insert_symbol") {
         this._insert_symbol(message.symbol);
       }
-      else if (message.command === "reset_control_symbols") {
-        this._reset_control_symbols();
+      else if (message.command === "reset_control") {
+        this._reset_control();
       }
       else if (message.command === "apply_control") {
-        this._apply_control_effect(message.action);
+        this._apply_control(message.action);
       }
     });
   }
 
-  private _apply_control_effect(action: string): void {
+  private _apply_control(action: string): void {
     const editor = window.activeTextEditor;
     if (!editor) return;
 
@@ -151,7 +151,7 @@
     textDecoration: "none"
   });
 
-  private _reset_control_symbols(): void {
+  private _reset_control(): void {
     const editor = window.activeTextEditor;
     if (!editor) {
       return;