--- 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