clarified protocol for "PIDE/sledgehammer_sendback" vs. "PIDE/sledgehammer_insert": rely on existing Isabelle/Scala/PIDE operations;

--- 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 {

--- 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))
     })

--- 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<void>("PIDE/sledgehammer_locate");
 
+export const sledgehammer_sendback_type =
+  new NotificationType<Sledgehammer_Sendback>("PIDE/sledgehammer_sendback");
+
 export const sledgehammer_insert_type =
-  new NotificationType<void>("PIDE/sledgehammer_insert");
+  new NotificationType<Sledgehammer_Insert>("PIDE/sledgehammer_insert");
 
 export const sledgehammer_provers_request_type =
   new NotificationType<void>("PIDE/sledgehammer_provers_request");
@@ -250,9 +256,6 @@
 export const sledgehammer_output_type =
   new NotificationType<Sledgehammer_Output>("PIDE/sledgehammer_output");
 
-export const sledgehammer_insert_position_response_type =
-  new NotificationType<SledgehammerInsertPosition>("PIDE/sledgehammer_insert_position_response");
-
 
 /* spell checker */
 

--- 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 });
     }
   }
 

--- 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")
         }

--- 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))
   }
 }

--- 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()