tuned whitespace;

--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 14:33:16 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 14:39:31 2025 +0100
@@ -3,7 +3,7 @@
   let was_cancelled = false;
   let can_be_cancelled = false;
 
-  let history = []; 
+  let history = [];
 
   const container = document.createElement('div');
   container.id = 'sledgehammer-container';
@@ -171,7 +171,7 @@
     was_cancelled = false;
     can_be_cancelled = true;
     result.innerHTML = '';
-    add_to_history(provers_input.value); 
+    add_to_history(provers_input.value);
     hide_dropdown();
     vscode.postMessage({
       command: 'apply',
@@ -232,7 +232,8 @@
       set_history(message.history);
       if (message.provers) {
         provers_input.value = message.provers;
-      } else if (message.history && message.history.length > 0) {
+      }
+      else if (message.history && message.history.length > 0) {
         provers_input.value = message.history[0];
       }
     }
@@ -268,7 +269,8 @@
                 span.textContent = text;
                 div.appendChild(span);
               }
-            } else if (node.nodeName.toLowerCase() === 'sendback') {
+            }
+            else if (node.nodeName.toLowerCase() === 'sendback') {
               const button = document.createElement('button');
               button.textContent = node.textContent.trim();
               button.addEventListener('click', () => {
@@ -296,7 +298,8 @@
       }
       if (/Unknown proof context/i.test(message.content)) {
         result.classList.add('error');
-      } else {
+      }
+      else {
         result.classList.remove('error');
       }
       can_be_cancelled = false;

--- a/src/Tools/VSCode/extension/media/symbols.js	Sun Oct 26 14:33:16 2025 +0100
+++ b/src/Tools/VSCode/extension/media/symbols.js	Sun Oct 26 14:39:31 2025 +0100
@@ -76,7 +76,8 @@
     const searchLimit = 50;
     if (matchingSymbols.length === 0) {
       resultsContainer.innerHTML = "<p>No symbols found</p>";
-    } else {
+    }
+    else {
       matchingSymbols.slice(0, searchLimit).forEach(symbol => {
         const decodedSymbol = decodeHtmlEntity(symbol.code);
         if (!decodedSymbol) return;
@@ -112,10 +113,12 @@
       if (char === "\u21e7") {
         i++;
         if (i < symbol.length) result += "<sup>" + symbol[i] + "</sup>";
-      } else if (char === "\u21e9") { 
+      }
+      else if (char === "\u21e9") { 
         i++;
         if (i < symbol.length) result += "<sub>" + symbol[i] + "</sub>";
-      } else {
+      }
+      else {
         result += char;
       }
       i++;
@@ -134,13 +137,15 @@
         if (controlSup) result += controlSup + symbol[i];
         else result += symbol[i];
       }
-    } else if (char === "\u21e9") {
+    }
+    else if (char === "\u21e9") {
       i++;
       if (i < symbol.length) {
         if (controlSub) result += controlSub + symbol[i];
         else result += symbol[i];
       }
-    } else {
+    }
+    else {
       result += char;
     }
     i++;
@@ -239,7 +244,8 @@
         const button = document.createElement('div');
         if (group === "arrow") {
           button.classList.add('arrow-button'); // special class for arrows
-        } else {
+        }
+        else {
           button.classList.add('symbol-button');
         }
         button.textContent = decodedSymbol;

--- a/src/Tools/VSCode/extension/src/symbol_panel.ts	Sun Oct 26 14:33:16 2025 +0100
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts	Sun Oct 26 14:39:31 2025 +0100
@@ -73,9 +73,11 @@
     this._view.webview.onDidReceiveMessage(message => {
       if (message.command === 'insertSymbol') {
         this._insert_symbol(message.symbol);
-      } else if (message.command === 'resetControlSymbols') {
+      }
+      else if (message.command === 'resetControlSymbols') {
         this._reset_control_symbols();
-      } else if (message.command === 'applyControl') {
+      }
+      else if (message.command === 'applyControl') {
         this._apply_control_effect(message.action);
       }
     });
@@ -113,7 +115,8 @@
       if (!selection.isEmpty) {
         if (action === "bold") {
           editor.setDecorations(this.boldDecoration, [{ range: selection }]);
-        } else {
+        }
+        else {
           let newText = selectedText
             .split("")
             .map((char, index, arr) => {
@@ -127,7 +130,8 @@
 
           editBuilder.replace(selection, newText);
         }
-      } else {
+      }
+      else {
         editBuilder.insert(selection.active, controlSymbol);
       }
     }).then(success => {