# HG changeset patch # User wenzelm # Date 1396525578 -7200 # Node ID 76acce58aeab90ea22377985bb073c9af962545f # Parent 5a93b8f928a29f7fe46530b5332e607daeff1148 more general prover operations; diff -r 5a93b8f928a2 -r 76acce58aeab src/Pure/PIDE/prover.scala --- /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 + } +} + diff -r 5a93b8f928a2 -r 76acce58aeab src/Pure/PIDE/session.scala --- 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) diff -r 5a93b8f928a2 -r 76acce58aeab src/Pure/System/invoke_scala.scala --- 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) => diff -r 5a93b8f928a2 -r 76acce58aeab 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(_)): _*) } diff -r 5a93b8f928a2 -r 76acce58aeab src/Pure/Tools/simplifier_trace.scala --- 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) diff -r 5a93b8f928a2 -r 76acce58aeab src/Pure/Tools/sledgehammer_params.scala --- 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 diff -r 5a93b8f928a2 -r 76acce58aeab src/Pure/build-jars --- 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 diff -r 5a93b8f928a2 -r 76acce58aeab src/Tools/jEdit/src/protocol_dockable.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) diff -r 5a93b8f928a2 -r 76acce58aeab src/Tools/jEdit/src/raw_output_dockable.scala --- 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") diff -r 5a93b8f928a2 -r 76acce58aeab src/Tools/jEdit/src/syslog_dockable.scala --- 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)