src/Pure/PIDE/prover.scala
changeset 82794 3db393729a65
parent 82144 e8959b23208b
child 83203 61277d1550d6
--- 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))