dismantle redundant sledgehammer history in Isabelle/Scala, which does not quite work --- and is already done via vscode.setState / vscode.getState;
proper message name for Sledgehammer_Provers;
discontinue pointless "init" flag;

--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 18:38:22 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 19:14:08 2025 +0100
@@ -73,7 +73,6 @@
           history = history.filter(h => h !== item);
           render_dropdown(false);
           show_dropdown();
-          vscode.postMessage({ command: "delete_prover_history", entry: item });
         });
 
         row.appendChild(delete_button);
@@ -120,12 +119,6 @@
     }
   });
 
-  function set_history(new_history) {
-    history = Array.isArray(new_history) ? new_history : [];
-    save_state();
-    render_dropdown(false);
-  }
-
   function save_state() {
     vscode.setState({
       history,
@@ -228,14 +221,8 @@
     if (message.command === "status") {
       spinner.classList.toggle("loading", message.message !== "Finished");
     }
-    else if (message.command === "provers") {
-      set_history(message.history);
-      if (message.provers) {
-        provers_input.value = message.provers;
-      }
-      else if (message.history && message.history.length > 0) {
-        provers_input.value = message.history[0];
-      }
+    else if (message.command === "provers" && message.provers) {
+      provers_input.value = message.provers;
     }
     else if (message.command === "no_proof_context") {
       const div = document.createElement("div");

--- a/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 18:38:22 2025 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sun Oct 26 19:14:08 2025 +0100
@@ -246,9 +246,8 @@
         sledgehammer_provider.insert(msg.position))
       language_client.onNotification(lsp.sledgehammer_locate_response_type, msg =>
         sledgehammer_provider.locate(msg.position))
-      language_client.onNotification(lsp.sledgehammer_provers_response, msg => {
-        sledgehammer_provider.update_provers(msg.provers, msg.history)
-      })
+      language_client.onNotification(lsp.sledgehammer_provers_response, msg =>
+        sledgehammer_provider.update_provers(msg.provers))
       language_client.onNotification(lsp.sledgehammer_no_proof_context_type, () =>
         sledgehammer_provider.updateNoProofContext());
     })

--- a/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 18:38:22 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Sun Oct 26 19:14:08 2025 +0100
@@ -237,11 +237,6 @@
 
 export interface Sledgehammer_Provers {
   provers: string;
-  history: string[];
-}
-
-export interface Sledgehammer_Provers_Delete {
-  entry: string;
 }
 
 export interface SledgehammerNoSuchProver {
@@ -251,14 +246,11 @@
 export const sledgehammer_request_type =
   new NotificationType<SledgehammerApplyRequest>("PIDE/sledgehammer_request");
 
-export const sledgehammer_provers_delete =
-  new NotificationType<Sledgehammer_Provers_Delete>("PIDE/sledgehammer_deleteProvers_request");
-
 export const sledgehammer_cancel_type =
   new NotificationType<void>("PIDE/sledgehammer_cancel_request");
 
 export const sledgehammer_provers =
-  new NotificationType<InitRequest>("PIDE/sledgehammer_provers_request");
+  new NotificationType<void>("PIDE/sledgehammer_provers_request");
 
 export const sledgehammer_provers_response =
   new NotificationType<Sledgehammer_Provers>("PIDE/sledgehammer_provers_response");

--- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 18:38:22 2025 +0100
+++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts	Sun Oct 26 19:14:08 2025 +0100
@@ -35,7 +35,7 @@
 
   request_provers(language_client: LanguageClient) {
     if (language_client) {
-      this._language_client.sendNotification(lsp.sledgehammer_provers, { init: true });
+      this._language_client.sendNotification(lsp.sledgehammer_provers);
     }
   }
 
@@ -83,13 +83,6 @@
           });
           this.text_to_insert = message.text;
           break;
-
-        case 'delete_prover_history':
-          this._language_client.sendNotification(lsp.sledgehammer_provers_delete, {
-            entry: message.entry
-          });
-          break;
-
       }
     });
   }
@@ -100,9 +93,9 @@
     }
   }
 
-  public update_provers(provers: string, history: string[]): void {
+  public update_provers(provers: string): void {
     if (this._view) {
-      this._view.webview.postMessage({ command: 'provers', provers, history });
+      this._view.webview.postMessage({ command: 'provers', provers });
     }
   }
 

--- a/src/Tools/VSCode/src/language_server.scala	Sun Oct 26 18:38:22 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Sun Oct 26 19:14:08 2025 +0100
@@ -98,7 +98,7 @@
 
 class Language_Server(
   val channel: Channel,
-  options: Options,
+  val options: Options,
   session_name: String = Language_Server.default_logic,
   include_sessions: List[String] = Nil,
   session_dirs: List[Path] = Nil,
@@ -552,9 +552,7 @@
           case LSP.Sledgehammer_Request(provers, isar, try0, purpose) =>
             sledgehammer.handle_request(provers, isar, try0, purpose)
           case LSP.Sledgehammer_Cancel => sledgehammer.cancel_query()
-          case LSP.Sledgehammer_Provers(init) => sledgehammer.send_provers_and_history(init)
-          case LSP.Sledgehammer_Delete_Prover(entry) =>
-            sledgehammer.handle_sledgehammer_delete(entry)
+          case LSP.Sledgehammer_Provers => sledgehammer.send_provers()
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }

--- a/src/Tools/VSCode/src/lsp.scala	Sun Oct 26 18:38:22 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Sun Oct 26 19:14:08 2025 +0100
@@ -811,14 +811,8 @@
 
   /* sledgehammer */
 
-  object Sledgehammer_Provers {
-    def unapply(json: JSON.T): Option[Boolean] =
-      json match {
-        case Notification("PIDE/documentation_request", Some(params)) =>
-          JSON.bool(params, "init")
-        case _ => None
-      }
-  }
+  object Sledgehammer_Provers
+    extends Notification0("PIDE/sledgehammer_provers_request")
 
   object Sledgehammer_Request {
     def unapply(json: JSON.T): Option[(String, Boolean, Boolean, Int)] =
@@ -834,23 +828,12 @@
       }
   }
 
-  object Sledgehammer_Delete_Prover {
-    def unapply(json: JSON.T): Option[String] =
-      json match {
-        case Notification("PIDE/sledgehammer_deleteProvers_request", Some(params)) =>
-          JSON.string(params, "entry")
-        case _ => None
-      }
-  }
-
   object Sledgehammer_Cancel
     extends Notification0("PIDE/sledgehammer_cancel_request")
 
   object Sledgehammer_Provers_Response {
-    def apply(provers: String, history: List[String]): JSON.T =
-      Notification(
-        "PIDE/sledgehammer_provers_response",
-        JSON.Object("provers" -> provers, "history" -> history))
+    def apply(provers: String): JSON.T =
+      Notification("PIDE/sledgehammer_provers_response", JSON.Object("provers" -> provers))
   }
 
   object Sledgehammer_NoProver_Response {

--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 18:38:22 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 19:14:08 2025 +0100
@@ -24,34 +24,13 @@
   var current_purpose: Int = 1
   private var last_sendback_id: Option[Int] = None
 
-  private val provers_history_option: String = "vscode_sledgehammer_history"
-  private val provers_history_delim: Char = ','
-
-  private var persistent_options: Options = Options.init()
-
-  private def get_provers_history(): List[String] =
-    Library.space_explode(provers_history_delim, persistent_options.string(provers_history_option)).filterNot(_.isEmpty)
-
-  private def set_provers_history(new_history: String): Unit = {
-    persistent_options = persistent_options.string.update(provers_history_option, new_history)
-    persistent_options.save_prefs()
-  }
-
-  def send_provers_and_history(init: Boolean): Unit = {
-    val provers = persistent_options.check_name("sledgehammer_provers").value
-    val history = get_provers_history()
-    server.channel.write(LSP.Sledgehammer_Provers_Response.apply(provers, history))
-  }
-
-  def add_provers_history(entry: String): Unit = {
-    val current = get_provers_history()
-    val history = (entry :: current.filter(_ != entry)).take(10)
-    val history_str = history.mkString(provers_history_delim.toString)
-    set_provers_history(history_str)
+  def send_provers(): Unit = {
+    val provers = server.options.string("sledgehammer_provers")
+    server.channel.write(LSP.Sledgehammer_Provers_Response.apply(provers))
   }
 
   def handle_request(provers: String, isar: Boolean, try0: Boolean, purpose: Int): Unit = {
-    val available_provers = Word.explode(persistent_options.string("sledgehammer_provers")).toSet
+    val available_provers = Word.explode(server.options.string("sledgehammer_provers")).toSet
     val user_provers = Word.explode(provers).toSet
     val invalid = user_provers.diff(available_provers)
     if (invalid.nonEmpty) {
@@ -59,17 +38,6 @@
       return
     }
     choose_purpose(List(provers, isar.toString, try0.toString), purpose)
-    add_provers_history(provers)
-  }
-
-  def handle_sledgehammer_delete(entry: String): Unit = {
-    val history = get_provers_history().filter(_ != entry)
-    val history_str = history.mkString(provers_history_delim.toString)
-    set_provers_history(history_str)
-  }
-
-  private def reload_persistent_options(): Unit = {
-    persistent_options = Options.init()
   }
 
   private def consume_status(status: Query_Operation.Status): Unit = {