tuned signature -- emphasize Isabelle_Process Input vs. Output;
--- a/src/Pure/System/isabelle_process.scala Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala Sat Mar 03 17:30:14 2012 +0100
@@ -18,7 +18,7 @@
object Isabelle_Process
{
- /* results */
+ /* messages */
object Kind
{
@@ -44,7 +44,7 @@
XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
}
- class Result(val message: XML.Elem) extends Message
+ class Output(val message: XML.Elem) extends Message
{
def kind: String = message.markup.name
def properties: Properties.T = message.markup.properties
@@ -84,29 +84,29 @@
import Isabelle_Process._
- /* results */
+ /* output */
- private def system_result(text: String)
+ private def system_output(text: String)
{
- receiver(new Result(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
+ receiver(new Output(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
}
private val xml_cache = new XML.Cache()
- private def put_result(kind: String, props: Properties.T, body: XML.Body)
+ private def output_message(kind: String, props: Properties.T, body: XML.Body)
{
if (kind == Isabelle_Markup.INIT) system_channel.accepted()
if (kind == Isabelle_Markup.RAW)
- receiver(new Result(XML.Elem(Markup(kind, props), body)))
+ receiver(new Output(XML.Elem(Markup(kind, props), body)))
else {
val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
- receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
+ receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
}
}
- private def put_result(kind: String, text: String)
+ private def output_message(kind: String, text: String)
{
- put_result(kind, Nil, List(XML.Text(Symbol.decode(text))))
+ output_message(kind, Nil, List(XML.Text(Symbol.decode(text))))
}
@@ -147,7 +147,7 @@
private def terminate_process()
{
try { process.terminate }
- catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
+ catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) }
}
private val process_manager = Simple_Thread.fork("process_manager")
@@ -169,10 +169,10 @@
}
(finished.isEmpty || !finished.get, result.toString.trim)
}
- if (startup_errors != "") system_result(startup_errors)
+ if (startup_errors != "") system_output(startup_errors)
if (startup_failed) {
- put_result(Isabelle_Markup.EXIT, "Return code: 127")
+ output_message(Isabelle_Markup.EXIT, "Return code: 127")
process.stdin.close
Thread.sleep(300)
terminate_process()
@@ -188,11 +188,11 @@
val message = message_actor(message_stream)
val rc = process_result.join
- system_result("process terminated")
+ system_output("process terminated")
for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
thread.join
- system_result("process_manager terminated")
- put_result(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
+ system_output("process_manager terminated")
+ output_message(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
}
system_channel.accepted()
}
@@ -205,7 +205,7 @@
def terminate()
{
close()
- system_result("Terminating Isabelle process")
+ system_output("Terminating Isabelle process")
terminate_process()
}
@@ -235,8 +235,8 @@
//}}}
}
}
- catch { case e: IOException => system_result(name + ": " + e.getMessage) }
- system_result(name + " terminated")
+ catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+ system_output(name + " terminated")
}
}
@@ -263,7 +263,7 @@
else done = true
}
if (result.length > 0) {
- put_result(markup, result.toString)
+ output_message(markup, result.toString)
result.length = 0
}
else {
@@ -273,8 +273,8 @@
//}}}
}
}
- catch { case e: IOException => system_result(name + ": " + e.getMessage) }
- system_result(name + " terminated")
+ catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+ system_output(name + " terminated")
}
}
@@ -304,8 +304,8 @@
//}}}
}
}
- catch { case e: IOException => system_result(name + ": " + e.getMessage) }
- system_result(name + " terminated")
+ catch { case e: IOException => system_output(name + ": " + e.getMessage) }
+ system_output(name + " terminated")
}
}
@@ -365,7 +365,7 @@
if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
val kind = Kind.message_markup(name(0))
val body = read_chunk(kind != Isabelle_Markup.RAW)
- put_result(kind, props, body)
+ output_message(kind, props, body)
case _ =>
read_chunk(false)
throw new Protocol_Error("bad header: " + header.toString)
@@ -376,12 +376,12 @@
} while (c != -1)
}
catch {
- case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
- case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
+ case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
+ case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
}
stream.close
- system_result(name + " terminated")
+ system_output(name + " terminated")
}
}
--- a/src/Pure/System/session.scala Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Pure/System/session.scala Sat Mar 03 17:30:14 2012 +0100
@@ -56,8 +56,8 @@
val caret_focus = new Event_Bus[Session.Caret_Focus.type]
val commands_changed = new Event_Bus[Session.Commands_Changed]
val phase_changed = new Event_Bus[Session.Phase]
- val syslog_messages = new Event_Bus[Isabelle_Process.Result]
- val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
+ val syslog_messages = new Event_Bus[Isabelle_Process.Output]
+ val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
val protocol_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
@@ -193,14 +193,14 @@
def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
buffer += msg
msg match {
- case result: Isabelle_Process.Result =>
- if (result.is_syslog)
+ case output: Isabelle_Process.Output =>
+ if (output.is_syslog)
syslog >> (queue =>
{
- val queue1 = queue.enqueue(result.message)
+ val queue1 = queue.enqueue(output.message)
if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
})
- if (result.is_raw) flush()
+ if (output.is_raw) flush()
case _ =>
}
}
@@ -343,34 +343,34 @@
//}}}
- /* prover results */
+ /* prover output */
- def handle_result(result: Isabelle_Process.Result)
+ def handle_output(output: Isabelle_Process.Output)
//{{{
{
- def bad_result(result: Isabelle_Process.Result)
+ def bad_output(output: Isabelle_Process.Output)
{
if (verbose)
- System.err.println("Ignoring prover result: " + result.message.toString)
+ System.err.println("Ignoring prover output: " + output.message.toString)
}
- result.properties match {
+ output.properties match {
- case Position.Id(state_id) if !result.is_raw =>
+ case Position.Id(state_id) if !output.is_raw =>
try {
- val st = global_state >>> (_.accumulate(state_id, result.message))
+ val st = global_state >>> (_.accumulate(state_id, output.message))
delay_commands_changed.invoke(st.command)
}
catch {
- case _: Document.State.Fail => bad_result(result)
+ case _: Document.State.Fail => bad_output(output)
}
- case Isabelle_Markup.Assign_Execs if result.is_raw =>
- XML.content(result.body).mkString match {
+ case Isabelle_Markup.Assign_Execs if output.is_raw =>
+ XML.content(output.body).mkString match {
case Protocol.Assign(id, assign) =>
try { handle_assign(id, assign) }
- catch { case _: Document.State.Fail => bad_result(result) }
- case _ => bad_result(result)
+ catch { case _: Document.State.Fail => bad_output(output) }
+ case _ => bad_output(output)
}
// FIXME separate timeout event/message!?
if (prover.isDefined && System.currentTimeMillis() > prune_next) {
@@ -379,44 +379,44 @@
prune_next = System.currentTimeMillis() + prune_delay.ms
}
- case Isabelle_Markup.Removed_Versions if result.is_raw =>
- XML.content(result.body).mkString match {
+ case Isabelle_Markup.Removed_Versions if output.is_raw =>
+ XML.content(output.body).mkString match {
case Protocol.Removed(removed) =>
try { handle_removed(removed) }
- catch { case _: Document.State.Fail => bad_result(result) }
- case _ => bad_result(result)
+ catch { case _: Document.State.Fail => bad_output(output) }
+ case _ => bad_output(output)
}
- case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
+ case Isabelle_Markup.Invoke_Scala(name, id) if output.is_raw =>
Future.fork {
- val arg = XML.content(result.body).mkString
+ val arg = XML.content(output.body).mkString
val (tag, res) = Invoke_Scala.method(name, arg)
prover.get.invoke_scala(id, tag, res)
}
- case Isabelle_Markup.Cancel_Scala(id) if result.is_raw =>
+ case Isabelle_Markup.Cancel_Scala(id) if output.is_raw =>
System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task
- case Isabelle_Markup.Ready if result.is_raw =>
+ case Isabelle_Markup.Ready if output.is_raw =>
// FIXME move to ML side (!?)
syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
phase = Session.Ready
- case Isabelle_Markup.Loaded_Theory(name) if result.is_raw =>
+ case Isabelle_Markup.Loaded_Theory(name) if output.is_raw =>
thy_load.register_thy(name)
- case Isabelle_Markup.Command_Decl(name, kind) if result.is_raw =>
+ case Isabelle_Markup.Command_Decl(name, kind) if output.is_raw =>
syntax += (name, kind)
- case Isabelle_Markup.Keyword_Decl(name) if result.is_raw =>
+ case Isabelle_Markup.Keyword_Decl(name) if output.is_raw =>
syntax += name
case _ =>
- if (result.is_exit && phase == Session.Startup) phase = Session.Failed
- else if (result.is_exit) phase = Session.Inactive
- else if (result.is_stdout) { }
- else bad_result(result)
+ if (output.is_exit && phase == Session.Startup) phase = Session.Failed
+ else if (output.is_exit) phase = Session.Inactive
+ else if (output.is_stdout) { }
+ else bad_output(output)
}
}
//}}}
@@ -473,11 +473,11 @@
case input: Isabelle_Process.Input =>
protocol_messages.event(input)
- case result: Isabelle_Process.Result =>
- handle_result(result)
- if (result.is_syslog) syslog_messages.event(result)
- if (result.is_stdout || result.is_stderr) raw_output_messages.event(result)
- protocol_messages.event(result)
+ case output: Isabelle_Process.Output =>
+ handle_output(output)
+ if (output.is_syslog) syslog_messages.event(output)
+ if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
+ protocol_messages.event(output)
}
case change: Change_Node
--- a/src/Tools/jEdit/src/protocol_dockable.scala Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Sat Mar 03 17:30:14 2012 +0100
@@ -31,8 +31,8 @@
case input: Isabelle_Process.Input =>
Swing_Thread.now { text_area.append(input.toString + "\n") }
- case result: Isabelle_Process.Result =>
- Swing_Thread.now { text_area.append(result.message.toString + "\n") }
+ case output: Isabelle_Process.Output =>
+ Swing_Thread.now { text_area.append(output.message.toString + "\n") }
case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Sat Mar 03 17:30:14 2012 +0100
@@ -29,9 +29,9 @@
private val main_actor = actor {
loop {
react {
- case result: Isabelle_Process.Result =>
- if (result.is_stdout || result.is_stderr)
- Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
+ case output: Isabelle_Process.Output =>
+ if (output.is_stdout || output.is_stderr)
+ Swing_Thread.now { text_area.append(XML.content(output.message).mkString) }
case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
}
--- a/src/Tools/jEdit/src/session_dockable.scala Sat Mar 03 16:59:30 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala Sat Mar 03 17:30:14 2012 +0100
@@ -173,8 +173,8 @@
private val main_actor = actor {
loop {
react {
- case result: Isabelle_Process.Result =>
- if (result.is_syslog)
+ case output: Isabelle_Process.Output =>
+ if (output.is_syslog)
Swing_Thread.now {
val text = Isabelle.session.current_syslog()
if (text != syslog.text) syslog.text = text