--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/prover.scala Thu Apr 03 13:46:18 2014 +0200
@@ -0,0 +1,58 @@
+/* Title: Pure/PIDE/prover.scala
+ Author: Makarius
+
+General prover operations.
+*/
+
+package isabelle
+
+
+object Prover
+{
+ /* 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
+ }
+}
+
--- a/src/Pure/PIDE/session.scala Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Pure/PIDE/session.scala Thu Apr 03 13:46:18 2014 +0200
@@ -56,12 +56,12 @@
abstract class Protocol_Handler
{
def stop(prover: Prover): Unit = {}
- val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean]
+ val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
}
class Protocol_Handlers(
handlers: Map[String, Session.Protocol_Handler] = Map.empty,
- functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty)
+ functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
{
def get(name: String): Option[Protocol_Handler] = handlers.get(name)
@@ -81,7 +81,7 @@
val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
val new_functions =
for ((a, f) <- new_handler.functions.toList) yield
- (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg))
+ (a, (msg: Prover.Protocol_Output) => f(prover, msg))
val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
@@ -98,7 +98,7 @@
new Protocol_Handlers(handlers2, functions2)
}
- def invoke(msg: Isabelle_Process.Protocol_Output): Boolean =
+ def invoke(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
case Markup.Function(a) if functions.isDefinedAt(a) =>
try { functions(a)(msg) }
@@ -146,9 +146,9 @@
val raw_edits = new Event_Bus[Session.Raw_Edits]
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.Output]
- val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
- val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
+ val syslog_messages = new Event_Bus[Prover.Output]
+ val raw_output_messages = new Event_Bus[Prover.Output]
+ val all_messages = new Event_Bus[Prover.Message] // potential bottle-neck
val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
@@ -261,7 +261,7 @@
private case class Start(args: List[String])
private case class Cancel_Exec(exec_id: Document_ID.Exec)
private case class Protocol_Command(name: String, args: List[String])
- private case class Messages(msgs: List[Isabelle_Process.Message])
+ private case class Messages(msgs: List[Prover.Message])
private case class Update_Options(options: Options)
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
@@ -275,22 +275,22 @@
object receiver
{
- private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+ private var buffer = new mutable.ListBuffer[Prover.Message]
private def flush(): Unit = synchronized {
if (!buffer.isEmpty) {
val msgs = buffer.toList
this_actor ! Messages(msgs)
- buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+ buffer = new mutable.ListBuffer[Prover.Message]
}
}
- def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
+ def invoke(msg: Prover.Message): Unit = synchronized {
msg match {
- case _: Isabelle_Process.Input =>
+ case _: Prover.Input =>
buffer += msg
- case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush =>
+ case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
flush()
- case output: Isabelle_Process.Output =>
+ case output: Prover.Output =>
buffer += msg
if (output.is_syslog)
syslog >> (queue =>
@@ -410,7 +410,7 @@
/* prover output */
- def handle_output(output: Isabelle_Process.Output)
+ def handle_output(output: Prover.Output)
//{{{
{
def bad_output()
@@ -431,7 +431,7 @@
}
output match {
- case msg: Isabelle_Process.Protocol_Output =>
+ case msg: Prover.Protocol_Output =>
val handled = _protocol_handlers.invoke(msg)
if (!handled) {
msg.properties match {
@@ -541,17 +541,17 @@
case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
prover.get.dialog_result(serial, result)
- handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
+ handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
case Protocol_Command(name, args) if prover.isDefined =>
prover.get.protocol_command(name, args:_*)
case Messages(msgs) =>
msgs foreach {
- case input: Isabelle_Process.Input =>
+ case input: Prover.Input =>
all_messages.event(input)
- case output: Isabelle_Process.Output =>
+ case output: Prover.Output =>
if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
else handle_output(output)
if (output.is_syslog) syslog_messages.event(output)
--- a/src/Pure/System/invoke_scala.scala Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Pure/System/invoke_scala.scala Thu Apr 03 13:46:18 2014 +0200
@@ -89,7 +89,7 @@
}
private def invoke_scala(
- prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized
+ prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized
{
msg.properties match {
case Markup.Invoke_Scala(name, id) =>
@@ -105,7 +105,7 @@
}
private def cancel_scala(
- prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized
+ prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized
{
msg.properties match {
case Markup.Cancel_Scala(id) =>
--- 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(_)): _*)
}
--- a/src/Pure/Tools/simplifier_trace.scala Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala Thu Apr 03 13:46:18 2014 +0200
@@ -300,7 +300,7 @@
class Handler extends Session.Protocol_Handler
{
- private def cancel(prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
+ private def cancel(prover: Session.Prover, msg: Prover.Protocol_Output): Boolean =
msg.properties match {
case Markup.Simp_Trace_Cancel(serial) =>
manager ! Cancel(serial)
--- a/src/Pure/Tools/sledgehammer_params.scala Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Pure/Tools/sledgehammer_params.scala Thu Apr 03 13:46:18 2014 +0200
@@ -37,7 +37,7 @@
def get_provers: String = synchronized { _provers }
private def sledgehammer_provers(
- prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
+ prover: Session.Prover, msg: Prover.Protocol_Output): Boolean =
{
update_provers(msg.text)
true
--- a/src/Pure/build-jars Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Pure/build-jars Thu Apr 03 13:46:18 2014 +0200
@@ -52,6 +52,7 @@
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
+ PIDE/prover.scala
PIDE/query_operation.scala
PIDE/resources.scala
PIDE/session.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Thu Apr 03 13:46:18 2014 +0200
@@ -26,10 +26,10 @@
private val main_actor = actor {
loop {
react {
- case input: Isabelle_Process.Input =>
+ case input: Prover.Input =>
Swing_Thread.later { text_area.append(input.toString + "\n") }
- case output: Isabelle_Process.Output =>
+ case output: Prover.Output =>
Swing_Thread.later { 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 Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Thu Apr 03 13:46:18 2014 +0200
@@ -26,7 +26,7 @@
private val main_actor = actor {
loop {
react {
- case output: Isabelle_Process.Output =>
+ case output: Prover.Output =>
Swing_Thread.later {
text_area.append(XML.content(output.message))
if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
--- a/src/Tools/jEdit/src/syslog_dockable.scala Thu Apr 03 10:51:24 2014 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Thu Apr 03 13:46:18 2014 +0200
@@ -37,7 +37,7 @@
private val main_actor = actor {
loop {
react {
- case output: Isabelle_Process.Output =>
+ case output: Prover.Output =>
if (output.is_syslog) Swing_Thread.later { update_syslog() }
case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)