# HG changeset patch
# User wenzelm
# Date 1761499609 -3600
# Node ID f32e9720b31d29953aa4f4b94569bdf5a11b2831
# Parent  c08765f8ceaf1c88a6daa11e486e8eb8fcb64f6a
tuned quotes: follow Isabelle majority style, instead of JS/TS;

diff -r c08765f8ceaf -r f32e9720b31d src/Tools/VSCode/extension/media/sledgehammer.js
--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 18:24:39 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 18:26:49 2025 +0100
@@ -5,79 +5,79 @@
 
   let history = [];
 
-  const container = document.createElement('div');
-  container.id = 'sledgehammer-container';
+  const container = document.createElement("div");
+  container.id = "sledgehammer-container";
 
-  const top_row = document.createElement('div');
-  top_row.classList.add('top-row');
+  const top_row = document.createElement("div");
+  top_row.classList.add("top-row");
 
-  const provers_label = document.createElement('label');
-  provers_label.textContent = 'Provers: ';
+  const provers_label = document.createElement("label");
+  provers_label.textContent = "Provers: ";
 
-  const provers_input_wrapper = document.createElement('div');
-  provers_input_wrapper.className = 'provers-input-wrapper';
+  const provers_input_wrapper = document.createElement("div");
+  provers_input_wrapper.className = "provers-input-wrapper";
 
-  const provers_input = document.createElement('input');
-  provers_input.type = 'text';
-  provers_input.id = 'provers';
+  const provers_input = document.createElement("input");
+  provers_input.type = "text";
+  provers_input.id = "provers";
   provers_input.size = 30;
-  provers_input.value = '';
-  provers_input.autocomplete = 'off';
+  provers_input.value = "";
+  provers_input.autocomplete = "off";
 
   provers_input_wrapper.appendChild(provers_input);
 
-  const chevron_button = document.createElement('button');
-  chevron_button.type = 'button';
-  chevron_button.className = 'provers-dropdown-toggle';
-  chevron_button.setAttribute('aria-label', 'Show provers history');
+  const chevron_button = document.createElement("button");
+  chevron_button.type = "button";
+  chevron_button.className = "provers-dropdown-toggle";
+  chevron_button.setAttribute("aria-label", "Show provers history");
   chevron_button.tabIndex = -1;
-  chevron_button.innerHTML = '\u25bc';
+  chevron_button.innerHTML = "\u25bc";
   provers_input_wrapper.appendChild(chevron_button);
 
   provers_label.appendChild(provers_input_wrapper);
 
-  const dropdown = document.createElement('div');
-  dropdown.className = 'provers-dropdown';
+  const dropdown = document.createElement("div");
+  dropdown.className = "provers-dropdown";
   provers_input_wrapper.appendChild(dropdown);
 
   function show_dropdown() {
-    dropdown.classList.add('visible');
+    dropdown.classList.add("visible");
   }
   function hide_dropdown() {
-    dropdown.classList.remove('visible');
+    dropdown.classList.remove("visible");
   }
 
   function render_dropdown(open = false) {
-    dropdown.innerHTML = '';
-    const header = document.createElement('div');
-    header.textContent = 'Previously entered strings:';
-    header.className = 'history-header';
+    dropdown.innerHTML = "";
+    const header = document.createElement("div");
+    header.textContent = "Previously entered strings:";
+    header.className = "history-header";
     dropdown.appendChild(header);
     if (history.length === 0) {
-      const no_entry = document.createElement('div');
-      no_entry.className = 'history-header';
+      const no_entry = document.createElement("div");
+      no_entry.className = "history-header";
     }
     else {
       history.forEach(item => {
-        const row = document.createElement('div');
+        const row = document.createElement("div");
         row.tabIndex = 0;
         row.textContent = item;
 
-        const delete_button = document.createElement('span');
-        delete_button.textContent = '\u2716';
-        delete_button.className = 'delete-btn';
-        delete_button.title = 'Delete entry';
-        delete_button.addEventListener('mousedown', function (ev) {
+        const delete_button = document.createElement("span");
+        delete_button.textContent = "\u2716";
+        delete_button.className = "delete-btn";
+        delete_button.title = "Delete entry";
+        delete_button.addEventListener("mousedown", function (ev) {
           ev.preventDefault();
           ev.stopPropagation();
           history = history.filter(h => h !== item);
           render_dropdown(false);
           show_dropdown();
-          vscode.postMessage({ command: 'delete_prover_history', entry: item });
+          vscode.postMessage({ command: "delete_prover_history", entry: item });
         });
 
         row.appendChild(delete_button);
-        row.addEventListener('mousedown', function (e) {
+        row.addEventListener("mousedown", function (e) {
           e.preventDefault();
           provers_input.value = item;
           hide_dropdown();
@@ -90,9 +90,9 @@
   }
 
 
-  chevron_button.addEventListener('mousedown', function (e) {
+  chevron_button.addEventListener("mousedown", function (e) {
     e.preventDefault();
-    if (dropdown.classList.contains('visible')) {
+    if (dropdown.classList.contains("visible")) {
       hide_dropdown();
     }
     else {
@@ -102,20 +102,20 @@
     }
   });
 
-  provers_input.addEventListener('input', () => { });
+  provers_input.addEventListener("input", () => { });
 
-  provers_input.addEventListener('focus', function () {
+  provers_input.addEventListener("focus", function () {
     render_dropdown(true);
     show_dropdown();
   });
-  provers_input.addEventListener('blur', () => {
+  provers_input.addEventListener("blur", () => {
     setTimeout(() => {
       if (!dropdown.contains(document.activeElement)) hide_dropdown();
     }, 150);
   });
 
-  provers_input.addEventListener('keydown', (e) => {
-    if (e.key === 'ArrowDown' && dropdown.childNodes.length) {
+  provers_input.addEventListener("keydown", (e) => {
+    if (e.key === "ArrowDown" && dropdown.childNodes.length) {
       dropdown.firstChild && dropdown.firstChild.focus && dropdown.firstChild.focus();
     }
   });
@@ -142,64 +142,64 @@
     render_dropdown();
   }
 
-  const isar_label = document.createElement('label');
-  const isar_checkbox = document.createElement('input');
-  isar_checkbox.type = 'checkbox';
-  isar_checkbox.id = 'isar';
+  const isar_label = document.createElement("label");
+  const isar_checkbox = document.createElement("input");
+  isar_checkbox.type = "checkbox";
+  isar_checkbox.id = "isar";
   isar_label.appendChild(isar_checkbox);
-  isar_label.appendChild(document.createTextNode(' Isar proofs'));
+  isar_label.appendChild(document.createTextNode(" Isar proofs"));
 
-  const try0_label = document.createElement('label');
-  const try0_checkbox = document.createElement('input');
-  try0_checkbox.type = 'checkbox';
-  try0_checkbox.id = 'try0';
+  const try0_label = document.createElement("label");
+  const try0_checkbox = document.createElement("input");
+  try0_checkbox.type = "checkbox";
+  try0_checkbox.id = "try0";
   try0_checkbox.checked = true;
   try0_label.appendChild(try0_checkbox);
-  try0_label.appendChild(document.createTextNode(' Try methods'));
+  try0_label.appendChild(document.createTextNode(" Try methods"));
 
 
-  provers_input.addEventListener('input', save_state);
-  isar_checkbox.addEventListener('change', save_state);
-  try0_checkbox.addEventListener('change', save_state);
-  const spinner = document.createElement('div');
-  spinner.id = 'sledgehammer-spinner';
+  provers_input.addEventListener("input", save_state);
+  isar_checkbox.addEventListener("change", save_state);
+  try0_checkbox.addEventListener("change", save_state);
+  const spinner = document.createElement("div");
+  spinner.id = "sledgehammer-spinner";
 
-  const apply_button = document.createElement('button');
-  apply_button.textContent = 'Apply';
-  apply_button.id = 'apply-btn';
-  apply_button.addEventListener('click', () => {
+  const apply_button = document.createElement("button");
+  apply_button.textContent = "Apply";
+  apply_button.id = "apply-btn";
+  apply_button.addEventListener("click", () => {
     was_cancelled = false;
     can_be_cancelled = true;
-    result.innerHTML = '';
+    result.innerHTML = "";
     add_to_history(provers_input.value);
     hide_dropdown();
     vscode.postMessage({
-      command: 'apply',
+      command: "apply",
       provers: provers_input.value,
       isar: isar_checkbox.checked,
       try0: try0_checkbox.checked
     });
   });
 
-  const cancel_button = document.createElement('button');
-  cancel_button.textContent = 'Cancel';
-  cancel_button.addEventListener('click', () => {
-    vscode.postMessage({ command: 'cancel' });
+  const cancel_button = document.createElement("button");
+  cancel_button.textContent = "Cancel";
+  cancel_button.addEventListener("click", () => {
+    vscode.postMessage({ command: "cancel" });
     if (was_cancelled) return;
     if (!can_be_cancelled) return;
     was_cancelled = true;
-    spinner.classList.remove('loading');
+    spinner.classList.remove("loading");
     const div = document.createElement("div");
     div.classList.add("interrupt");
     div.textContent = "Interrupt";
     result.appendChild(div);
   });
 
-  const locate_button = document.createElement('button');
-  locate_button.textContent = 'Locate';
-  locate_button.addEventListener('click', () => {
+  const locate_button = document.createElement("button");
+  locate_button.textContent = "Locate";
+  locate_button.addEventListener("click", () => {
     vscode.postMessage({
-      command: 'locate',
+      command: "locate",
       provers: provers_input.value,
       isar: isar_checkbox.checked,
       try0: try0_checkbox.checked
@@ -215,20 +215,20 @@
   top_row.appendChild(locate_button);
   container.appendChild(top_row);
 
-  const result = document.createElement('div');
-  result.id = 'result';
+  const result = document.createElement("div");
+  result.id = "result";
   container.appendChild(result);
 
   document.body.appendChild(container);
 
   render_dropdown();
 
-  window.addEventListener('message', event => {
+  window.addEventListener("message", event => {
     const message = event.data;
-    if (message.command === 'status') {
-      spinner.classList.toggle('loading', message.message !== "Finished");
+    if (message.command === "status") {
+      spinner.classList.toggle("loading", message.message !== "Finished");
     }
-    else if (message.command === 'provers') {
+    else if (message.command === "provers") {
       set_history(message.history);
       if (message.provers) {
         provers_input.value = message.provers;
@@ -237,45 +237,45 @@
         provers_input.value = message.history[0];
       }
     }
-    else if (message.command === 'no_proof_context') {
+    else if (message.command === "no_proof_context") {
       const div = document.createElement("div");
       div.classList.add("interrupt");
       div.textContent = "Unknown proof context";
       result.appendChild(div);
     }
-    else if (message.command === 'no_provers') {
+    else if (message.command === "no_provers") {
       const div = document.createElement("div");
       div.classList.add("interrupt");
       div.textContent = "No such provers";
       result.appendChild(div);
     }
-    else if (message.command === 'result') {
+    else if (message.command === "result") {
       if (was_cancelled) return;
-      result.innerHTML = '';
+      result.innerHTML = "";
       const parser = new DOMParser();
-      const xml_doc = parser.parseFromString(`<root>${message.content}</root>`, 'application/xml');
-      const messages = xml_doc.getElementsByTagName('writeln_message');
+      const xml_doc = parser.parseFromString(`<root>${message.content}</root>`, "application/xml");
+      const messages = xml_doc.getElementsByTagName("writeln_message");
       for (const msg of messages) {
-        const div = document.createElement('div');
+        const div = document.createElement("div");
         const inner = msg.innerHTML;
-        if (inner.includes('<sendback')) {
-          const temp_container = document.createElement('div');
+        if (inner.includes("<sendback")) {
+          const temp_container = document.createElement("div");
           temp_container.innerHTML = inner;
           temp_container.childNodes.forEach(node => {
             if (node.nodeType === Node.TEXT_NODE) {
               const text = node.textContent.trim();
               if (text) {
-                const span = document.createElement('span');
+                const span = document.createElement("span");
                 span.textContent = text;
                 div.appendChild(span);
               }
             }
-            else if (node.nodeName.toLowerCase() === 'sendback') {
-              const button = document.createElement('button');
+            else if (node.nodeName.toLowerCase() === "sendback") {
+              const button = document.createElement("button");
               button.textContent = node.textContent.trim();
-              button.addEventListener('click', () => {
+              button.addEventListener("click", () => {
                 vscode.postMessage({
-                  command: 'insert_text',
+                  command: "insert_text",
                   provers: provers_input.value,
                   isar: isar_checkbox.checked,
                   try0: try0_checkbox.checked,
@@ -285,7 +285,7 @@
               div.appendChild(button);
             }
             else {
-              const span = document.createElement('span');
+              const span = document.createElement("span");
               span.textContent = node.textContent.trim();
               div.appendChild(span);
             }
@@ -297,10 +297,10 @@
         result.appendChild(div);
       }
       if (/Unknown proof context/i.test(message.content)) {
-        result.classList.add('error');
+        result.classList.add("error");
       }
       else {
-        result.classList.remove('error');
+        result.classList.remove("error");
       }
       can_be_cancelled = false;
     }
@@ -310,7 +310,7 @@
     const saved = vscode.getState();
     if (saved) {
       history = Array.isArray(saved.history) ? saved.history : [];
-      provers_input.value = saved.provers || '';
+      provers_input.value = saved.provers || "";
       isar_checkbox.checked = !!saved.isar;
       try0_checkbox.checked = saved.try0 !== undefined ? saved.try0 : true;
       render_dropdown(false);