# HG changeset patch # User wenzelm # Date 1762095392 -3600 # Node ID 62178604511c91ab179db5f62a250e016432b60d # Parent d9059089359b0f1586dbce0699e96fa4f725e7e0 clarified protocol for "PIDE/sledgehammer_sendback" vs. "PIDE/sledgehammer_insert": rely on existing Isabelle/Scala/PIDE operations; diff -r d9059089359b -r 62178604511c src/Tools/VSCode/extension/media/sledgehammer.js --- a/src/Tools/VSCode/extension/media/sledgehammer.js Sun Nov 02 15:53:25 2025 +0100 +++ b/src/Tools/VSCode/extension/media/sledgehammer.js Sun Nov 02 15:56:32 2025 +0100 @@ -217,7 +217,7 @@ const button = document.createElement("button"); button.textContent = node.textContent.trim(); button.addEventListener("click", () => - vscode.postMessage({ command: "insert", text: node.textContent.trim() })); + vscode.postMessage({ command: "sendback", text: node.textContent.trim() })); div.appendChild(button); } else { diff -r d9059089359b -r 62178604511c src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Sun Nov 02 15:53:25 2025 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Sun Nov 02 15:56:32 2025 +0100 @@ -240,8 +240,8 @@ sledgehammer_provider.update_status(msg.message)) language_client.onNotification(lsp.sledgehammer_output_type, msg => sledgehammer_provider.update_output(msg)) - language_client.onNotification(lsp.sledgehammer_insert_position_response_type, msg => - sledgehammer_provider.insert(msg.position)) + language_client.onNotification(lsp.sledgehammer_insert_type, msg => + sledgehammer_provider.insert(msg)) language_client.onNotification(lsp.sledgehammer_provers_response_type, msg => sledgehammer_provider.update_provers(msg.provers)) }) diff -r d9059089359b -r 62178604511c src/Tools/VSCode/extension/src/lsp.ts --- a/src/Tools/VSCode/extension/src/lsp.ts Sun Nov 02 15:53:25 2025 +0100 +++ b/src/Tools/VSCode/extension/src/lsp.ts Sun Nov 02 15:56:32 2025 +0100 @@ -214,12 +214,15 @@ }; } -export interface SledgehammerInsertPosition { - position: { - uri: string; - line: number; - character: number; - }; +export interface Sledgehammer_Sendback { + text: string; +} + +export interface Sledgehammer_Insert { + uri: string; + line: number; + character: number; + text: string; } export interface Sledgehammer_Provers { @@ -235,8 +238,11 @@ export const sledgehammer_locate_type = new NotificationType("PIDE/sledgehammer_locate"); +export const sledgehammer_sendback_type = + new NotificationType("PIDE/sledgehammer_sendback"); + export const sledgehammer_insert_type = - new NotificationType("PIDE/sledgehammer_insert"); + new NotificationType("PIDE/sledgehammer_insert"); export const sledgehammer_provers_request_type = new NotificationType("PIDE/sledgehammer_provers_request"); @@ -250,9 +256,6 @@ export const sledgehammer_output_type = new NotificationType("PIDE/sledgehammer_output"); -export const sledgehammer_insert_position_response_type = - new NotificationType("PIDE/sledgehammer_insert_position_response"); - /* spell checker */ diff -r d9059089359b -r 62178604511c src/Tools/VSCode/extension/src/sledgehammer_panel.ts --- a/src/Tools/VSCode/extension/src/sledgehammer_panel.ts Sun Nov 02 15:53:25 2025 +0100 +++ b/src/Tools/VSCode/extension/src/sledgehammer_panel.ts Sun Nov 02 15:56:32 2025 +0100 @@ -17,8 +17,6 @@ class Sledgehammer_Panel_Provider implements WebviewViewProvider { public static readonly view_type = "isabelle-sledgehammer"; private _view?: WebviewView; - private _result_position?: { uri: string; line: number; character: number; line_text: string }; - private text_to_insert: string; constructor( private readonly _extension_uri: Uri, @@ -71,9 +69,9 @@ case "locate": this._language_client.sendNotification(lsp.sledgehammer_locate_type); break; - case "insert": - this._language_client.sendNotification(lsp.sledgehammer_insert_type); - this.text_to_insert = message.text; + case "sendback": + this._language_client.sendNotification(lsp.sledgehammer_sendback_type, + { text: message.text }); break; } }); @@ -102,31 +100,20 @@ } } - public insert(position: { uri: string; line: number; character: number }): void { + public insert(arg: { uri: string; line: number; character: number; text: string }): void { + const uri = Uri.parse(arg.uri); const editor = window.activeTextEditor; - if (editor) { - const uri = Uri.parse(position.uri); - if (editor.document.uri.toString() === uri.toString()) { - const pos = new Position(position.line, position.character); - const line_text = editor.document.lineAt(pos.line).text; - const text_to_insert = - line_text.trim() === "" ? this.text_to_insert : "\n" + this.text_to_insert; - editor.edit(edit_builder => edit_builder.insert(pos, text_to_insert)); - } + if (editor && editor.document.uri.toString() === uri.toString()) { + const pos = new Position(arg.line, arg.character); + const line_text = editor.document.lineAt(pos.line).text; + editor.edit(edit_builder => + edit_builder.insert(pos, line_text.trim() === "" ? arg.text : "\n" + arg.text)); } } public update_output(result: lsp.Sledgehammer_Output): void { - const editor = window.activeTextEditor; - const line_text = editor?.document.lineAt(result.position.line).text ?? ""; - this._result_position = { ...result.position, line_text }; if (this._view) { - this._view.webview.postMessage({ - command: "result", - content: result.content, - position: result.position, - sendback_id: result.sendback_id - }); + this._view.webview.postMessage({ command: "result", content: result.content }); } } diff -r d9059089359b -r 62178604511c src/Tools/VSCode/src/language_server.scala --- a/src/Tools/VSCode/src/language_server.scala Sun Nov 02 15:53:25 2025 +0100 +++ b/src/Tools/VSCode/src/language_server.scala Sun Nov 02 15:56:32 2025 +0100 @@ -542,7 +542,7 @@ case LSP.Sledgehammer_Request(args) => sledgehammer.request(args) case LSP.Sledgehammer_Cancel() => sledgehammer.cancel() case LSP.Sledgehammer_Locate() => sledgehammer.locate() - case LSP.Sledgehammer_Insert() => sledgehammer.insert() + case LSP.Sledgehammer_Sendback(text) => sledgehammer.sendback(text) case LSP.Sledgehammer_Provers_Request() => sledgehammer.send_provers() case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED") } diff -r d9059089359b -r 62178604511c src/Tools/VSCode/src/lsp.scala --- a/src/Tools/VSCode/src/lsp.scala Sun Nov 02 15:53:25 2025 +0100 +++ b/src/Tools/VSCode/src/lsp.scala Sun Nov 02 15:56:32 2025 +0100 @@ -822,18 +822,30 @@ } object Sledgehammer_Output { - def apply(json: JSON.Object.T): JSON.T = - Notification("PIDE/sledgehammer_output", json) + def apply(content: String): JSON.T = + Notification("PIDE/sledgehammer_output", JSON.Object("content" -> content)) } object Sledgehammer_Cancel extends Notification0("PIDE/sledgehammer_cancel") object Sledgehammer_Locate extends Notification0("PIDE/sledgehammer_locate") - object Sledgehammer_Insert extends Notification0("PIDE/sledgehammer_insert") + object Sledgehammer_Sendback { + def unapply(json: JSON.T): Option[String] = + json match { + case Notification("PIDE/sledgehammer_sendback", Some(params)) => + JSON.string(params, "text") + case _ => None + } + } - object Sledgehammer_Insert_Position_Response { - def apply(json: JSON.Object.T): JSON.T = - Notification("PIDE/sledgehammer_insert_position_response", json) + object Sledgehammer_Insert { + def apply(node_pos: Line.Node_Position, text: String): JSON.T = + Notification("PIDE/sledgehammer_insert", + JSON.Object( + "uri" -> Url.print_file_name(node_pos.name), + "line" -> node_pos.pos.line, + "character" -> node_pos.pos.column, + "text" -> text)) } } diff -r d9059089359b -r 62178604511c src/Tools/VSCode/src/vscode_sledgehammer.scala --- a/src/Tools/VSCode/src/vscode_sledgehammer.scala Sun Nov 02 15:53:25 2025 +0100 +++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala Sun Nov 02 15:56:32 2025 +0100 @@ -15,8 +15,6 @@ private val query_operation = new Query_Operation(server.editor, (), "sledgehammer", consume_status, consume_output) - private var last_sendback_id: Option[Int] = None - def send_provers(): Unit = { val provers = server.options.string("sledgehammer_provers") server.channel.write(LSP.Sledgehammer_Provers_Response.apply(provers)) @@ -32,130 +30,25 @@ server.channel.write(LSP.Sledgehammer_Status(msg)) } - private def extract_sendback_id(body: List[XML.Elem]): Option[Int] = { - def traverse(tree: XML.Tree): Option[Int] = tree match { - case XML.Elem(markup, body) if markup.name == "sendback" => - markup.properties.find(_._1 == "id").flatMap { - case (_, id_str) => scala.util.Try(id_str.toInt).toOption - }.orElse(body.view.flatMap(traverse).headOption) - - case XML.Elem(_, body) => - body.view.flatMap(traverse).headOption - - case _ => None - } - body.view.flatMap(traverse).headOption - } - - private def count_lines(text: String, offset: Int): Int = - text.substring(0, offset).count(_ == '\n') - - private def count_column(text: String, offset: Int): Int = { - val last_newline = text.substring(0, offset).lastIndexOf('\n') - if (last_newline >= 0) offset - last_newline - 1 else offset - } - - private def resolve_position( - snapshot: Document.Snapshot, - sendback_id: Int - ): Option[(String, Int, Int)] = { - snapshot.node.commands.find(_.id == sendback_id).flatMap { command => - snapshot.node.command_iterator().find(_._1 == command).map { - case (_, start_offset) => - val end_offset = start_offset + command.length - val text = snapshot.node.source - val line = count_lines(text, end_offset) - val column = count_column(text, end_offset) - val uri = Url.print_file(new java.io.File(snapshot.node_name.node)) - (uri, line, column) - } - } - } - - private def query_position_from_sendback( - snapshot: Document.Snapshot, - sendback_id: Int - ): Option[(String, Int, Int)] = { - val node = snapshot.node - val iterator = node.command_iterator().toList - - iterator.find(_._1.id == sendback_id).map { case (command, start_offset) => - val text = node.source - val line = count_lines(text, start_offset) - val column = count_column(text, start_offset) - val uri = Url.print_file(new java.io.File(snapshot.node_name.node)) - - val snippet = - text.substring(start_offset, (start_offset + command.length).min(text.length)) - .replace("\n", "\\n") - - (uri, line, column) - } - } - private def consume_output(output: Editor.Output): Unit = { - val snapshot = output.snapshot - val body = output.messages - - val sendback_id_opt = extract_sendback_id(body) - last_sendback_id = sendback_id_opt - - val position = sendback_id_opt.flatMap(id => resolve_position(snapshot, id)) - .getOrElse(("unknown", 0, 0)) - - val query_position = sendback_id_opt.flatMap(id => query_position_from_sendback(snapshot, id)) - .getOrElse(("unknown", 0, 0)) - - val json = JSON.Object( - "content" -> XML.string_of_body(body), - "position" -> JSON.Object( - "uri" -> position._1, - "line" -> position._2, - "character" -> position._3 - ), - "sendback_id" -> sendback_id_opt.getOrElse(-1), - "state_location" -> JSON.Object( - "uri" -> query_position._1, - "line" -> query_position._2, - "character" -> query_position._3) - ) - server.channel.write(LSP.Sledgehammer_Output(json)) - } - - def insert(): Unit = { - last_sendback_id match { - case Some(sendback_id) => - val models = server.resources.get_models() - val model_opt = models.find { model => - val snapshot = server.resources.snapshot(model) - val contains = snapshot.node.commands.exists(_.id == sendback_id) - contains - } - - model_opt match { - case Some(model) => - val snapshot = server.resources.snapshot(model) - resolve_position(snapshot, sendback_id) match { - case Some((uri, line, col)) => - val json = JSON.Object( - "position" -> JSON.Object( - "uri" -> uri, - "line" -> line, - "character" -> col - ) - ) - server.channel.write(LSP.Sledgehammer_Insert_Position_Response(json)) - case None => - } - case None => - } - case None => - } + val content = XML.string_of_body(output.messages) + server.channel.write(LSP.Sledgehammer_Output(content)) } def request(args: List[String]): Unit = server.editor.send_dispatcher { query_operation.apply_query(args) } + def sendback(text: String): Unit = + server.editor.send_dispatcher { + for { + (snapshot, command) <- query_operation.query_command() + node_pos <- snapshot.find_command_position(command.id, 0) + } { + val node_pos1 = node_pos.advance(command.source(command.core_range)) + server.channel.write(LSP.Sledgehammer_Insert(node_pos1, text)) + } + } + def cancel(): Unit = server.editor.send_dispatcher { query_operation.cancel_query() } def locate(): Unit = server.editor.send_dispatcher { query_operation.locate_query() } def init(): Unit = query_operation.activate()