# HG changeset patch
# User wenzelm
# Date 1719830454 -7200
# Node ID 7a1f9e57104655d71c0057ec6f8615090d0f2474
# Parent  38d020af64aa3186ee3f576371d46a0a18ce3742
clarified signature: more explicit XML.Body types, more uniform Symbol.encode_yxml;

diff -r 38d020af64aa -r 7a1f9e571046 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -240,7 +240,7 @@
                   }
                   catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) }
 
-                session.protocol_command("Prover.stop", rc.toString)
+                session.protocol_command("Prover.stop", XML.Encode.int(rc))
                 Build_Session_Errors(errors)
                 true
               }
@@ -360,17 +360,16 @@
             Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
               Exn.capture { process.await_startup() } match {
                 case Exn.Res(_) =>
-                  val resources_yxml = resources.init_session_yxml
+                  val resources_xml = resources.init_session_xml
                   val encode_options: XML.Encode.T[Options] =
                     options => session.prover_options(options).encode
-                  val args_yxml =
-                    YXML.string_of_body(
-                      {
-                        import XML.Encode._
-                        pair(string, list(pair(encode_options, list(pair(string, properties)))))(
-                          (session_name, info.theories))
-                      })
-                  session.protocol_command("build_session", resources_yxml, args_yxml)
+                  val args_xml =
+                    {
+                      import XML.Encode._
+                      pair(string, list(pair(encode_options, list(pair(string, properties)))))(
+                        (session_name, info.theories))
+                    }
+                  session.protocol_command("build_session", resources_xml, args_xml)
                   Build_Session_Errors.result
                 case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
               }
diff -r 38d020af64aa -r 7a1f9e571046 src/Pure/Build/resources.scala
--- a/src/Pure/Build/resources.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/Build/resources.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -37,23 +37,22 @@
 
   /* init session */
 
-  def init_session_yxml: String = {
+  def init_session_xml: XML.Body = {
     import XML.Encode._
 
-    YXML.string_of_body(
-      pair(list(pair(string, properties)),
-      pair(list(pair(string, string)),
-      pair(list(properties),
-      pair(list(pair(string, properties)),
-      pair(list(Scala.encode_fun),
-      pair(list(pair(string, string)), list(string)))))))(
-       (sessions_structure.session_positions,
-       (sessions_structure.dest_session_directories,
-       (command_timings,
-       (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
-       (Scala.functions,
-       (sessions_structure.global_theories.toList,
-        session_base.loaded_theories.keys))))))))
+    pair(list(pair(string, properties)),
+    pair(list(pair(string, string)),
+    pair(list(properties),
+    pair(list(pair(string, properties)),
+    pair(list(Scala.encode_fun),
+    pair(list(pair(string, string)), list(string)))))))(
+     (sessions_structure.session_positions,
+     (sessions_structure.dest_session_directories,
+     (command_timings,
+     (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
+     (Scala.functions,
+     (sessions_structure.global_theories.toList,
+      session_base.loaded_theories.keys)))))))
   }
 
 
diff -r 38d020af64aa -r 7a1f9e571046 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/ML/ml_process.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -86,7 +86,7 @@
     val eval_init_session = if (session_heaps.isEmpty) Nil else List("Resources.init_session_env ()")
     val init_session = Isabelle_System.tmp_file("init_session")
     File.restrict(File.path(init_session))
-    File.write(init_session, new Resources(session_background).init_session_yxml)
+    File.write(init_session, YXML.string_of_body(new Resources(session_background).init_session_xml))
 
     // process
     val eval_process =
diff -r 38d020af64aa -r 7a1f9e571046 src/Pure/PIDE/document_id.scala
--- a/src/Pure/PIDE/document_id.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/PIDE/document_id.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -20,4 +20,6 @@
 
   def apply(id: Generic): String = Value.Long.apply(id)
   def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
+
+  def encode(id: Generic): XML.Body = XML.Encode.long(id)
 }
diff -r 38d020af64aa -r 7a1f9e571046 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -307,20 +307,20 @@
   /* protocol commands */
 
   def protocol_command_raw(name: String, args: List[Bytes]): Unit
-  def protocol_command_args(name: String, args: List[String]): Unit
-  def protocol_command(name: String, args: String*): Unit
+  def protocol_command_args(name: String, args: List[XML.Body]): Unit
+  def protocol_command(name: String, args: XML.Body*): Unit
 
 
   /* options */
 
   def options(opts: Options): Unit =
-    protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
+    protocol_command("Prover.options", opts.encode)
 
 
   /* resources */
 
   def init_session(resources: Resources): Unit =
-    protocol_command("Prover.init_session", resources.init_session_yxml)
+    protocol_command("Prover.init_session", resources.init_session_xml)
 
 
   /* interned items */
@@ -331,13 +331,13 @@
   private def encode_command(
     resources: Resources,
     command: Command
-  ) : (String, String, String, String, String, List[String]) = {
+  ) : (XML.Body, XML.Body, XML.Body, XML.Body, XML.Body, List[XML.Body]) = {
     import XML.Encode._
 
     val parents = command.theory_parents(resources).map(name => File.standard_url(name.node))
-    val parents_yxml = Symbol.encode_yxml(list(string)(parents))
+    val parents_xml: XML.Body = list(string)(parents)
 
-    val blobs_yxml = {
+    val blobs_xml: XML.Body = {
       val encode_blob: T[Exn.Result[Command.Blob]] =
         variant(List(
           { case Exn.Res(Command.Blob(a, b, c)) =>
@@ -345,37 +345,31 @@
                 (a.node, b.implode, c.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
 
-      Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
+      pair(list(encode_blob), int)(command.blobs, command.blobs_index)
     }
 
-    val toks_yxml = {
+    val toks_xml: XML.Body = {
       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
-      Symbol.encode_yxml(list(encode_tok)(command.span.content))
+      list(encode_tok)(command.span.content)
     }
-    val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source))
+    val toks_sources_xml: List[XML.Body] = command.span.content.map(tok => XML.string(tok.source))
 
-    (Document_ID(command.id), Symbol.encode(command.span.name), parents_yxml,
-      blobs_yxml, toks_yxml, toks_sources)
+    (Document_ID.encode(command.id), XML.string(command.span.name),
+      parents_xml, blobs_xml, toks_xml, toks_sources_xml)
   }
 
   def define_command(resources: Resources, command: Command): Unit = {
-    val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
-      encode_command(resources, command)
-    protocol_command_args(
-      "Document.define_command", command_id :: name :: parents_yxml :: blobs_yxml ::
-        toks_yxml :: toks_sources)
+    val (a, b, c, d, e, rest) = encode_command(resources, command)
+    protocol_command_args("Document.define_command", a :: b :: c :: d :: e :: rest)
   }
 
   def define_commands(resources: Resources, commands: List[Command]): Unit =
     protocol_command_args("Document.define_commands",
       commands.map { command =>
         import XML.Encode._
-        val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
-          encode_command(resources, command)
-        val body =
-          pair(string, pair(string, pair(string, pair(string, pair(string, list(string))))))(
-            command_id, (name, (parents_yxml, (blobs_yxml, (toks_yxml, toks_sources)))))
-        YXML.string_of_body(body)
+        val (a, b, c, d, e, rest) = encode_command(resources, command)
+        pair(self, pair(self, pair(self, pair(self, pair(self, list(self))))))(
+          a, (b, (c, (d, (e, rest)))))
       })
 
   def define_commands_bulk(resources: Resources, commands: List[Command]): Unit = {
@@ -395,7 +389,7 @@
     protocol_command("Document.discontinue_execution")
 
   def cancel_exec(id: Document_ID.Exec): Unit =
-    protocol_command("Document.cancel_exec", Document_ID(id))
+    protocol_command("Document.cancel_exec", Document_ID.encode(id))
 
 
   /* document versions */
@@ -406,12 +400,10 @@
     edits: List[Document.Edit_Command],
     consolidate: List[Document.Node.Name]
   ): Unit = {
-    val consolidate_yxml = {
+    val consolidate_xml = { import XML.Encode._; list(string)(consolidate.map(_.node)) }
+    val edits_xml = {
       import XML.Encode._
-      Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
-    }
-    val edits_yxml = {
-      import XML.Encode._
+
       def id: T[Command] = (cmd => long(cmd.id))
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
@@ -428,23 +420,19 @@
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(string, list(string))))(c.dest)) }))
-      edits.map({ case (name, edit) =>
-        Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) })
+      edits.map({ case (name, edit) => pair(string, encode_edit(name))(name.node, edit) })
     }
     protocol_command_args("Document.update",
-      Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml)
+      Document_ID.encode(old_id) :: Document_ID.encode(new_id) :: consolidate_xml :: edits_xml)
   }
 
-  def remove_versions(versions: List[Document.Version]): Unit = {
-    val versions_yxml =
-    { import XML.Encode._
-      Symbol.encode_yxml(list(long)(versions.map(_.id))) }
-    protocol_command("Document.remove_versions", versions_yxml)
-  }
+  def remove_versions(versions: List[Document.Version]): Unit =
+    protocol_command("Document.remove_versions",
+      XML.Encode.list(Document_ID.encode)(versions.map(_.id)))
 
 
   /* dialog via document content */
 
   def dialog_result(serial: Long, result: String): Unit =
-    protocol_command("Document.dialog_result", Value.Long(serial), result)
+    protocol_command("Document.dialog_result", XML.Encode.long(serial), XML.string(result))
 }
diff -r 38d020af64aa -r 7a1f9e571046 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/PIDE/prover.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -17,11 +17,10 @@
   sealed abstract class Message
   type Receiver = Message => Unit
 
-  class Input(val name: String, val args: List[String]) extends Message {
+  class Input(val name: String, val args: List[XML.Body]) extends Message {
     override def toString: String =
       XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
-        args.flatMap(s =>
-          List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s))))).toString
+        args.flatMap(arg => List(XML.newline, XML.elem(Markup.PROVER_ARG, arg)))).toString
   }
 
   class Output(val message: XML.Elem) extends Message {
@@ -296,11 +295,11 @@
       case _ => error("Inactive prover input thread for command " + quote(name))
     }
 
-  def protocol_command_args(name: String, args: List[String]): Unit = {
+  def protocol_command_args(name: String, args: List[XML.Body]): Unit = {
     receiver(new Prover.Input(name, args))
-    protocol_command_raw(name, args.map(Bytes(_)))
+    protocol_command_raw(name, args.map(arg => Bytes(Symbol.encode_yxml(arg))))
   }
 
-  def protocol_command(name: String, args: String*): Unit =
+  def protocol_command(name: String, args: XML.Body*): Unit =
     protocol_command_args(name, args.toList)
 }
diff -r 38d020af64aa -r 7a1f9e571046 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 =
diff -r 38d020af64aa -r 7a1f9e571046 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -189,7 +189,7 @@
   def set_break(b: Boolean): Unit = {
     state.change { st =>
       val st1 = st.set_break(b)
-      session.protocol_command("Debugger.break", b.toString)
+      session.protocol_command("Debugger.break", XML.Encode.bool(b))
       st1
     }
     delay_update.invoke()
@@ -208,10 +208,10 @@
       val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint)
       session.protocol_command(
         "Debugger.breakpoint",
-        Symbol.encode(command.node_name.node),
-        Document_ID(command.id),
-        Value.Long(breakpoint),
-        Value.Boolean(breakpoint_state))
+        XML.string(command.node_name.node),
+        Document_ID.encode(command.id),
+        XML.Encode.long(breakpoint),
+        XML.Encode.bool(breakpoint_state))
       st1
     }
   }
@@ -238,7 +238,7 @@
   }
 
   def input(thread_name: String, msg: String*): Unit =
-    session.protocol_command_args("Debugger.input", thread_name :: msg.toList)
+    session.protocol_command_args("Debugger.input", (thread_name :: msg.toList).map(XML.string))
 
   def continue(thread_name: String): Unit = input(thread_name, "continue")
   def step(thread_name: String): Unit = input(thread_name, "step")
diff -r 38d020af64aa -r 7a1f9e571046 src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -158,7 +158,7 @@
 
     def do_reply(session: Session, serial: Long, answer: Answer): Unit = {
       session.protocol_command(
-        "Simplifier_Trace.reply", Value.Long(serial), answer.name)
+        "Simplifier_Trace.reply", XML.Encode.long(serial), XML.string(answer.name))
     }
 
     Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(