src/Pure/PIDE/session.scala

--- a/src/Pure/PIDE/session.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/PIDE/session.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -212,7 +212,7 @@
   private case class Get_State(promise: Promise[Document.State])
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command_Raw(name: String, args: List[Bytes])
-  private case class Protocol_Command_Args(name: String, args: List[String])
+  private case class Protocol_Command_Args(name: String, args: List[XML.Body])
   private case class Update_Options(options: Options)
   private case object Consolidate_Execution
   private case object Prune_History
@@ -550,7 +550,8 @@
                 }
                 catch {
                   case exn: Throwable =>
-                    prover.get.protocol_command("Prover.stop", "1", Exn.message(exn))
+                    prover.get.protocol_command(
+                      "Prover.stop", XML.Encode.int(1), XML.string(Exn.message(exn)))
                     false
                 }
 
@@ -750,10 +751,10 @@
   def protocol_command_raw(name: String, args: List[Bytes]): Unit =
     manager.send(Protocol_Command_Raw(name, args))
 
-  def protocol_command_args(name: String, args: List[String]): Unit =
+  def protocol_command_args(name: String, args: List[XML.Body]): Unit =
     manager.send(Protocol_Command_Args(name, args))
 
-  def protocol_command(name: String, args: String*): Unit =
+  def protocol_command(name: String, args: XML.Body*): Unit =
     protocol_command_args(name, args.toList)
 
   def cancel_exec(exec_id: Document_ID.Exec): Unit =