57 chunks match { |
57 chunks match { |
58 case List(chunk) => chunk |
58 case List(chunk) => chunk |
59 case _ => throw new Malformed("single chunk expected: " + print) |
59 case _ => throw new Malformed("single chunk expected: " + print) |
60 } |
60 } |
61 |
61 |
|
62 class System_Output(text: String) extends |
|
63 Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))) |
|
64 |
62 class Protocol_Output(props: Properties.T, val chunks: List[Bytes]) |
65 class Protocol_Output(props: Properties.T, val chunks: List[Bytes]) |
63 extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil)) { |
66 extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil)) { |
64 def chunk: Bytes = the_chunk(chunks, toString) |
67 def chunk: Bytes = the_chunk(chunks, toString) |
65 lazy val text: String = chunk.text |
68 lazy val text: String = chunk.text |
66 } |
69 } |
73 channel: System_Channel, |
76 channel: System_Channel, |
74 process: Bash.Process |
77 process: Bash.Process |
75 ) extends Protocol { |
78 ) extends Protocol { |
76 /** receiver output **/ |
79 /** receiver output **/ |
77 |
80 |
78 private def system_output(text: String): Unit = { |
81 private def system_output(text: String): Unit = |
79 receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))) |
82 receiver(new Prover.System_Output(text)) |
80 } |
83 |
81 |
84 private def protocol_output(props: Properties.T, chunks: List[Bytes]): Unit = |
82 private def protocol_output(props: Properties.T, chunks: List[Bytes]): Unit = { |
|
83 receiver(new Prover.Protocol_Output(props, chunks)) |
85 receiver(new Prover.Protocol_Output(props, chunks)) |
84 } |
|
85 |
86 |
86 private def output(kind: String, props: Properties.T, body: XML.Body): Unit = { |
87 private def output(kind: String, props: Properties.T, body: XML.Body): Unit = { |
87 val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body)) |
88 val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body)) |
88 val reports = Protocol_Message.reports(props, body) |
89 val reports = Protocol_Message.reports(props, body) |
89 for (msg <- main :: reports) receiver(new Prover.Output(cache.elem(msg))) |
90 for (msg <- main :: reports) receiver(new Prover.Output(cache.elem(msg))) |