more general prover operations;
authorwenzelm
Thu Apr 03 13:46:18 2014 +0200 (2014-04-03)
changeset 5638576acce58aeab
parent 56376 5a93b8f928a2
child 56386 fe520afb8041
more general prover operations;
src/Pure/PIDE/prover.scala
src/Pure/PIDE/session.scala
src/Pure/System/invoke_scala.scala
src/Pure/System/isabelle_process.scala
src/Pure/Tools/simplifier_trace.scala
src/Pure/Tools/sledgehammer_params.scala
src/Pure/build-jars
src/Tools/jEdit/src/protocol_dockable.scala
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/syslog_dockable.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/prover.scala	Thu Apr 03 13:46:18 2014 +0200
     1.3 @@ -0,0 +1,58 @@
     1.4 +/*  Title:      Pure/PIDE/prover.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +General prover operations.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Prover
    1.14 +{
    1.15 +  /* messages */
    1.16 +
    1.17 +  sealed abstract class Message
    1.18 +
    1.19 +  class Input(name: String, args: List[String]) extends Message
    1.20 +  {
    1.21 +    override def toString: String =
    1.22 +      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    1.23 +        args.map(s =>
    1.24 +          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    1.25 +  }
    1.26 +
    1.27 +  class Output(val message: XML.Elem) extends Message
    1.28 +  {
    1.29 +    def kind: String = message.markup.name
    1.30 +    def properties: Properties.T = message.markup.properties
    1.31 +    def body: XML.Body = message.body
    1.32 +
    1.33 +    def is_init = kind == Markup.INIT
    1.34 +    def is_exit = kind == Markup.EXIT
    1.35 +    def is_stdout = kind == Markup.STDOUT
    1.36 +    def is_stderr = kind == Markup.STDERR
    1.37 +    def is_system = kind == Markup.SYSTEM
    1.38 +    def is_status = kind == Markup.STATUS
    1.39 +    def is_report = kind == Markup.REPORT
    1.40 +    def is_syslog = is_init || is_exit || is_system || is_stderr
    1.41 +
    1.42 +    override def toString: String =
    1.43 +    {
    1.44 +      val res =
    1.45 +        if (is_status || is_report) message.body.map(_.toString).mkString
    1.46 +        else Pretty.string_of(message.body)
    1.47 +      if (properties.isEmpty)
    1.48 +        kind.toString + " [[" + res + "]]"
    1.49 +      else
    1.50 +        kind.toString + " " +
    1.51 +          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
    1.52 +    }
    1.53 +  }
    1.54 +
    1.55 +  class Protocol_Output(props: Properties.T, val bytes: Bytes)
    1.56 +    extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
    1.57 +  {
    1.58 +    lazy val text: String = bytes.toString
    1.59 +  }
    1.60 +}
    1.61 +
     2.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 03 10:51:24 2014 +0200
     2.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 03 13:46:18 2014 +0200
     2.3 @@ -56,12 +56,12 @@
     2.4    abstract class Protocol_Handler
     2.5    {
     2.6      def stop(prover: Prover): Unit = {}
     2.7 -    val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean]
     2.8 +    val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
     2.9    }
    2.10  
    2.11    class Protocol_Handlers(
    2.12      handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    2.13 -    functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty)
    2.14 +    functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
    2.15    {
    2.16      def get(name: String): Option[Protocol_Handler] = handlers.get(name)
    2.17  
    2.18 @@ -81,7 +81,7 @@
    2.19            val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
    2.20            val new_functions =
    2.21              for ((a, f) <- new_handler.functions.toList) yield
    2.22 -              (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg))
    2.23 +              (a, (msg: Prover.Protocol_Output) => f(prover, msg))
    2.24  
    2.25            val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    2.26            if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    2.27 @@ -98,7 +98,7 @@
    2.28        new Protocol_Handlers(handlers2, functions2)
    2.29      }
    2.30  
    2.31 -    def invoke(msg: Isabelle_Process.Protocol_Output): Boolean =
    2.32 +    def invoke(msg: Prover.Protocol_Output): Boolean =
    2.33        msg.properties match {
    2.34          case Markup.Function(a) if functions.isDefinedAt(a) =>
    2.35            try { functions(a)(msg) }
    2.36 @@ -146,9 +146,9 @@
    2.37    val raw_edits = new Event_Bus[Session.Raw_Edits]
    2.38    val commands_changed = new Event_Bus[Session.Commands_Changed]
    2.39    val phase_changed = new Event_Bus[Session.Phase]
    2.40 -  val syslog_messages = new Event_Bus[Isabelle_Process.Output]
    2.41 -  val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
    2.42 -  val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
    2.43 +  val syslog_messages = new Event_Bus[Prover.Output]
    2.44 +  val raw_output_messages = new Event_Bus[Prover.Output]
    2.45 +  val all_messages = new Event_Bus[Prover.Message]  // potential bottle-neck
    2.46    val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
    2.47  
    2.48  
    2.49 @@ -261,7 +261,7 @@
    2.50    private case class Start(args: List[String])
    2.51    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    2.52    private case class Protocol_Command(name: String, args: List[String])
    2.53 -  private case class Messages(msgs: List[Isabelle_Process.Message])
    2.54 +  private case class Messages(msgs: List[Prover.Message])
    2.55    private case class Update_Options(options: Options)
    2.56  
    2.57    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    2.58 @@ -275,22 +275,22 @@
    2.59  
    2.60      object receiver
    2.61      {
    2.62 -      private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
    2.63 +      private var buffer = new mutable.ListBuffer[Prover.Message]
    2.64  
    2.65        private def flush(): Unit = synchronized {
    2.66          if (!buffer.isEmpty) {
    2.67            val msgs = buffer.toList
    2.68            this_actor ! Messages(msgs)
    2.69 -          buffer = new mutable.ListBuffer[Isabelle_Process.Message]
    2.70 +          buffer = new mutable.ListBuffer[Prover.Message]
    2.71          }
    2.72        }
    2.73 -      def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
    2.74 +      def invoke(msg: Prover.Message): Unit = synchronized {
    2.75          msg match {
    2.76 -          case _: Isabelle_Process.Input =>
    2.77 +          case _: Prover.Input =>
    2.78              buffer += msg
    2.79 -          case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush =>
    2.80 +          case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
    2.81              flush()
    2.82 -          case output: Isabelle_Process.Output =>
    2.83 +          case output: Prover.Output =>
    2.84              buffer += msg
    2.85              if (output.is_syslog)
    2.86                syslog >> (queue =>
    2.87 @@ -410,7 +410,7 @@
    2.88  
    2.89      /* prover output */
    2.90  
    2.91 -    def handle_output(output: Isabelle_Process.Output)
    2.92 +    def handle_output(output: Prover.Output)
    2.93      //{{{
    2.94      {
    2.95        def bad_output()
    2.96 @@ -431,7 +431,7 @@
    2.97        }
    2.98  
    2.99        output match {
   2.100 -        case msg: Isabelle_Process.Protocol_Output =>
   2.101 +        case msg: Prover.Protocol_Output =>
   2.102            val handled = _protocol_handlers.invoke(msg)
   2.103            if (!handled) {
   2.104              msg.properties match {
   2.105 @@ -541,17 +541,17 @@
   2.106  
   2.107          case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
   2.108            prover.get.dialog_result(serial, result)
   2.109 -          handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
   2.110 +          handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
   2.111  
   2.112          case Protocol_Command(name, args) if prover.isDefined =>
   2.113            prover.get.protocol_command(name, args:_*)
   2.114  
   2.115          case Messages(msgs) =>
   2.116            msgs foreach {
   2.117 -            case input: Isabelle_Process.Input =>
   2.118 +            case input: Prover.Input =>
   2.119                all_messages.event(input)
   2.120  
   2.121 -            case output: Isabelle_Process.Output =>
   2.122 +            case output: Prover.Output =>
   2.123                if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
   2.124                else handle_output(output)
   2.125                if (output.is_syslog) syslog_messages.event(output)
     3.1 --- a/src/Pure/System/invoke_scala.scala	Thu Apr 03 10:51:24 2014 +0200
     3.2 +++ b/src/Pure/System/invoke_scala.scala	Thu Apr 03 13:46:18 2014 +0200
     3.3 @@ -89,7 +89,7 @@
     3.4    }
     3.5  
     3.6    private def invoke_scala(
     3.7 -    prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized
     3.8 +    prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized
     3.9    {
    3.10      msg.properties match {
    3.11        case Markup.Invoke_Scala(name, id) =>
    3.12 @@ -105,7 +105,7 @@
    3.13    }
    3.14  
    3.15    private def cancel_scala(
    3.16 -    prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized
    3.17 +    prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized
    3.18    {
    3.19      msg.properties match {
    3.20        case Markup.Cancel_Scala(id) =>
     4.1 --- a/src/Pure/System/isabelle_process.scala	Thu Apr 03 10:51:24 2014 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Apr 03 13:46:18 2014 +0200
     4.3 @@ -16,63 +16,10 @@
     4.4  import Actor._
     4.5  
     4.6  
     4.7 -object Isabelle_Process
     4.8 -{
     4.9 -  /* messages */
    4.10 -
    4.11 -  sealed abstract class Message
    4.12 -
    4.13 -  class Input(name: String, args: List[String]) extends Message
    4.14 -  {
    4.15 -    override def toString: String =
    4.16 -      XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    4.17 -        args.map(s =>
    4.18 -          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    4.19 -  }
    4.20 -
    4.21 -  class Output(val message: XML.Elem) extends Message
    4.22 -  {
    4.23 -    def kind: String = message.markup.name
    4.24 -    def properties: Properties.T = message.markup.properties
    4.25 -    def body: XML.Body = message.body
    4.26 -
    4.27 -    def is_init = kind == Markup.INIT
    4.28 -    def is_exit = kind == Markup.EXIT
    4.29 -    def is_stdout = kind == Markup.STDOUT
    4.30 -    def is_stderr = kind == Markup.STDERR
    4.31 -    def is_system = kind == Markup.SYSTEM
    4.32 -    def is_status = kind == Markup.STATUS
    4.33 -    def is_report = kind == Markup.REPORT
    4.34 -    def is_syslog = is_init || is_exit || is_system || is_stderr
    4.35 -
    4.36 -    override def toString: String =
    4.37 -    {
    4.38 -      val res =
    4.39 -        if (is_status || is_report) message.body.map(_.toString).mkString
    4.40 -        else Pretty.string_of(message.body)
    4.41 -      if (properties.isEmpty)
    4.42 -        kind.toString + " [[" + res + "]]"
    4.43 -      else
    4.44 -        kind.toString + " " +
    4.45 -          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
    4.46 -    }
    4.47 -  }
    4.48 -
    4.49 -  class Protocol_Output(props: Properties.T, val bytes: Bytes)
    4.50 -    extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
    4.51 -  {
    4.52 -    lazy val text: String = bytes.toString
    4.53 -  }
    4.54 -}
    4.55 -
    4.56 -
    4.57  class Isabelle_Process(
    4.58 -    receiver: Isabelle_Process.Message => Unit = Console.println(_),
    4.59 +    receiver: Prover.Message => Unit = Console.println(_),
    4.60      arguments: List[String] = Nil)
    4.61  {
    4.62 -  import Isabelle_Process._
    4.63 -
    4.64 -
    4.65    /* text representation */
    4.66  
    4.67    def encode(s: String): String = Symbol.encode(s)
    4.68 @@ -90,12 +37,12 @@
    4.69  
    4.70    private def system_output(text: String)
    4.71    {
    4.72 -    receiver(new Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
    4.73 +    receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
    4.74    }
    4.75  
    4.76    private def protocol_output(props: Properties.T, bytes: Bytes)
    4.77    {
    4.78 -    receiver(new Protocol_Output(props, bytes))
    4.79 +    receiver(new Prover.Protocol_Output(props, bytes))
    4.80    }
    4.81  
    4.82    private def output(kind: String, props: Properties.T, body: XML.Body)
    4.83 @@ -104,7 +51,7 @@
    4.84  
    4.85      val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
    4.86      val reports = Protocol.message_reports(props, body)
    4.87 -    for (msg <- main :: reports) receiver(new Output(xml_cache.elem(msg)))
    4.88 +    for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
    4.89    }
    4.90  
    4.91    private def exit_message(rc: Int)
    4.92 @@ -382,7 +329,7 @@
    4.93  
    4.94    def protocol_command(name: String, args: String*)
    4.95    {
    4.96 -    receiver(new Input(name, args.toList))
    4.97 +    receiver(new Prover.Input(name, args.toList))
    4.98      protocol_command_raw(name, args.map(Bytes(_)): _*)
    4.99    }
   4.100  
     5.1 --- a/src/Pure/Tools/simplifier_trace.scala	Thu Apr 03 10:51:24 2014 +0200
     5.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Thu Apr 03 13:46:18 2014 +0200
     5.3 @@ -300,7 +300,7 @@
     5.4  
     5.5    class Handler extends Session.Protocol_Handler
     5.6    {
     5.7 -    private def cancel(prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
     5.8 +    private def cancel(prover: Session.Prover, msg: Prover.Protocol_Output): Boolean =
     5.9        msg.properties match {
    5.10          case Markup.Simp_Trace_Cancel(serial) =>
    5.11            manager ! Cancel(serial)
     6.1 --- a/src/Pure/Tools/sledgehammer_params.scala	Thu Apr 03 10:51:24 2014 +0200
     6.2 +++ b/src/Pure/Tools/sledgehammer_params.scala	Thu Apr 03 13:46:18 2014 +0200
     6.3 @@ -37,7 +37,7 @@
     6.4      def get_provers: String = synchronized { _provers }
     6.5  
     6.6      private def sledgehammer_provers(
     6.7 -      prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
     6.8 +      prover: Session.Prover, msg: Prover.Protocol_Output): Boolean =
     6.9      {
    6.10        update_provers(msg.text)
    6.11        true
     7.1 --- a/src/Pure/build-jars	Thu Apr 03 10:51:24 2014 +0200
     7.2 +++ b/src/Pure/build-jars	Thu Apr 03 13:46:18 2014 +0200
     7.3 @@ -52,6 +52,7 @@
     7.4    PIDE/markup.scala
     7.5    PIDE/markup_tree.scala
     7.6    PIDE/protocol.scala
     7.7 +  PIDE/prover.scala
     7.8    PIDE/query_operation.scala
     7.9    PIDE/resources.scala
    7.10    PIDE/session.scala
     8.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Thu Apr 03 10:51:24 2014 +0200
     8.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Thu Apr 03 13:46:18 2014 +0200
     8.3 @@ -26,10 +26,10 @@
     8.4    private val main_actor = actor {
     8.5      loop {
     8.6        react {
     8.7 -        case input: Isabelle_Process.Input =>
     8.8 +        case input: Prover.Input =>
     8.9            Swing_Thread.later { text_area.append(input.toString + "\n") }
    8.10  
    8.11 -        case output: Isabelle_Process.Output =>
    8.12 +        case output: Prover.Output =>
    8.13            Swing_Thread.later { text_area.append(output.message.toString + "\n") }
    8.14  
    8.15          case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
     9.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Thu Apr 03 10:51:24 2014 +0200
     9.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Thu Apr 03 13:46:18 2014 +0200
     9.3 @@ -26,7 +26,7 @@
     9.4    private val main_actor = actor {
     9.5      loop {
     9.6        react {
     9.7 -        case output: Isabelle_Process.Output =>
     9.8 +        case output: Prover.Output =>
     9.9            Swing_Thread.later {
    9.10              text_area.append(XML.content(output.message))
    9.11              if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
    10.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Thu Apr 03 10:51:24 2014 +0200
    10.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Thu Apr 03 13:46:18 2014 +0200
    10.3 @@ -37,7 +37,7 @@
    10.4    private val main_actor = actor {
    10.5      loop {
    10.6        react {
    10.7 -        case output: Isabelle_Process.Output =>
    10.8 +        case output: Prover.Output =>
    10.9            if (output.is_syslog) Swing_Thread.later { update_syslog() }
   10.10  
   10.11          case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)