src/Pure/System/isabelle_process.scala

--- a/src/Pure/System/isabelle_process.scala	Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Apr 03 13:46:18 2014 +0200
@@ -16,63 +16,10 @@
 import Actor._
 
 
-object Isabelle_Process
-{
-  /* messages */
-
-  sealed abstract class Message
-
-  class Input(name: String, args: List[String]) extends Message
-  {
-    override def toString: String =
-      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
-        args.map(s =>
-          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
-  }
-
-  class Output(val message: XML.Elem) extends Message
-  {
-    def kind: String = message.markup.name
-    def properties: Properties.T = message.markup.properties
-    def body: XML.Body = message.body
-
-    def is_init = kind == Markup.INIT
-    def is_exit = kind == Markup.EXIT
-    def is_stdout = kind == Markup.STDOUT
-    def is_stderr = kind == Markup.STDERR
-    def is_system = kind == Markup.SYSTEM
-    def is_status = kind == Markup.STATUS
-    def is_report = kind == Markup.REPORT
-    def is_syslog = is_init || is_exit || is_system || is_stderr
-
-    override def toString: String =
-    {
-      val res =
-        if (is_status || is_report) message.body.map(_.toString).mkString
-        else Pretty.string_of(message.body)
-      if (properties.isEmpty)
-        kind.toString + " [[" + res + "]]"
-      else
-        kind.toString + " " +
-          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
-    }
-  }
-
-  class Protocol_Output(props: Properties.T, val bytes: Bytes)
-    extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
-  {
-    lazy val text: String = bytes.toString
-  }
-}
-
-
 class Isabelle_Process(
-    receiver: Isabelle_Process.Message => Unit = Console.println(_),
+    receiver: Prover.Message => Unit = Console.println(_),
     arguments: List[String] = Nil)
 {
-  import Isabelle_Process._
-
-
   /* text representation */
 
   def encode(s: String): String = Symbol.encode(s)
@@ -90,12 +37,12 @@
 
   private def system_output(text: String)
   {
-    receiver(new Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
+    receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
   private def protocol_output(props: Properties.T, bytes: Bytes)
   {
-    receiver(new Protocol_Output(props, bytes))
+    receiver(new Prover.Protocol_Output(props, bytes))
   }
 
   private def output(kind: String, props: Properties.T, body: XML.Body)
@@ -104,7 +51,7 @@
 
     val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
     val reports = Protocol.message_reports(props, body)
-    for (msg <- main :: reports) receiver(new Output(xml_cache.elem(msg)))
+    for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
   }
 
   private def exit_message(rc: Int)
@@ -382,7 +329,7 @@
 
   def protocol_command(name: String, args: String*)
   {
-    receiver(new Input(name, args.toList))
+    receiver(new Prover.Input(name, args.toList))
     protocol_command_raw(name, args.map(Bytes(_)): _*)
   }