# HG changeset patch # User wenzelm # Date 1761502448 -3600 # Node ID 1d9b1ca7977ea423371319e4a6bf2819b3ad769f # Parent 448f13c3efc3fa6cb56118636860702ad91246b3 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; diff -r 448f13c3efc3 -r 1d9b1ca7977e src/Tools/VSCode/extension/media/sledgehammer.js --- 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"); diff -r 448f13c3efc3 -r 1d9b1ca7977e src/Tools/VSCode/extension/src/extension.ts --- 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()); }) diff -r 448f13c3efc3 -r 1d9b1ca7977e src/Tools/VSCode/extension/src/lsp.ts --- 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("PIDE/sledgehammer_request"); -export const sledgehammer_provers_delete = - new NotificationType("PIDE/sledgehammer_deleteProvers_request"); - export const sledgehammer_cancel_type = new NotificationType("PIDE/sledgehammer_cancel_request"); export const sledgehammer_provers = - new NotificationType("PIDE/sledgehammer_provers_request"); + new NotificationType("PIDE/sledgehammer_provers_request"); export const sledgehammer_provers_response = new NotificationType("PIDE/sledgehammer_provers_response"); diff -r 448f13c3efc3 -r 1d9b1ca7977e src/Tools/VSCode/extension/src/sledgehammer_panel.ts --- 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 }); } } diff -r 448f13c3efc3 -r 1d9b1ca7977e src/Tools/VSCode/src/language_server.scala --- 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") } } diff -r 448f13c3efc3 -r 1d9b1ca7977e src/Tools/VSCode/src/lsp.scala --- 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 { diff -r 448f13c3efc3 -r 1d9b1ca7977e src/Tools/VSCode/src/vscode_sledgehammer.scala --- 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 = {