diff -r e78d50e3e1eb -r c7849fa2ece0 src/Tools/VSCode/extension/media/sledgehammer.js --- a/src/Tools/VSCode/extension/media/sledgehammer.js Mon Oct 27 12:15:14 2025 +0100 +++ b/src/Tools/VSCode/extension/media/sledgehammer.js Mon Oct 27 12:37:31 2025 +0100 @@ -190,14 +190,7 @@ const locate_button = document.createElement("button"); locate_button.textContent = "Locate"; - locate_button.addEventListener("click", () => { - vscode.postMessage({ - command: "locate", - provers: provers_input.value, - isar: isar_checkbox.checked, - try0: try0_checkbox.checked - }); - }); + locate_button.addEventListener("click", () => vscode.postMessage({ command: "locate" })); top_row.appendChild(provers_label); top_row.appendChild(isar_label);