# HG changeset patch
# User wenzelm
# Date 1751204893 -7200
# Node ID 3db393729a65801b4702deef20d43187b2ef1a2b
# Parent  fe8598c92be7b539a52582e76ff323b845b99ab9
tuned signature: more operations;

diff -r fe8598c92be7 -r 3db393729a65 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sun Jun 29 14:17:49 2025 +0200
+++ b/src/Pure/PIDE/prover.scala	Sun Jun 29 15:48:13 2025 +0200
@@ -59,6 +59,9 @@
       case _ => throw new Malformed("single chunk expected: " + print)
     }
 
+  class System_Output(text: String) extends
+    Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
+
   class Protocol_Output(props: Properties.T, val chunks: List[Bytes])
   extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil)) {
     def chunk: Bytes = the_chunk(chunks, toString)
@@ -75,13 +78,11 @@
 ) extends Protocol {
   /** receiver output **/
 
-  private def system_output(text: String): Unit = {
-    receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
-  }
+  private def system_output(text: String): Unit =
+    receiver(new Prover.System_Output(text))
 
-  private def protocol_output(props: Properties.T, chunks: List[Bytes]): Unit = {
+  private def protocol_output(props: Properties.T, chunks: List[Bytes]): Unit =
     receiver(new Prover.Protocol_Output(props, chunks))
-  }
 
   private def output(kind: String, props: Properties.T, body: XML.Body): Unit = {
     val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
diff -r fe8598c92be7 -r 3db393729a65 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun Jun 29 14:17:49 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Sun Jun 29 15:48:13 2025 +0200
@@ -810,6 +810,9 @@
     }
   }
 
+  def system_output(text: String): Unit =
+    manager.send(new Prover.System_Output(text))
+
   def protocol_command_raw(name: String, args: List[Bytes]): Unit =
     manager.send(Protocol_Command_Raw(name, args))