more general prover operations;
authorwenzelm
Thu Apr 03 14:54:17 2014 +0200 (2014-04-03 ago)
changeset 56387d92eb5c3960d
parent 56386 fe520afb8041
child 56388 c771f0fe28d1
more general prover operations;
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/resources.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/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/protocol.ML	Thu Apr 03 13:49:37 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Apr 03 14:54:17 2014 +0200
     1.3 @@ -8,11 +8,11 @@
     1.4  struct
     1.5  
     1.6  val _ =
     1.7 -  Isabelle_Process.protocol_command "Isabelle_Process.echo"
     1.8 +  Isabelle_Process.protocol_command "Prover.echo"
     1.9      (fn args => List.app writeln args);
    1.10  
    1.11  val _ =
    1.12 -  Isabelle_Process.protocol_command "Isabelle_Process.options"
    1.13 +  Isabelle_Process.protocol_command "Prover.options"
    1.14      (fn [options_yxml] =>
    1.15        let val options = Options.decode (YXML.parse_body options_yxml) in
    1.16          Options.set_default options;
     2.1 --- a/src/Pure/PIDE/protocol.scala	Thu Apr 03 13:49:37 2014 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Apr 03 14:54:17 2014 +0200
     2.3 @@ -325,15 +325,18 @@
     2.4  }
     2.5  
     2.6  
     2.7 -trait Protocol extends Isabelle_Process
     2.8 +trait Protocol extends Prover
     2.9  {
    2.10 -  /* inlined files */
    2.11 +  /* options */
    2.12 +
    2.13 +  def options(opts: Options): Unit =
    2.14 +    protocol_command("Prover.options", YXML.string_of_body(opts.encode))
    2.15 +
    2.16 +
    2.17 +  /* interned items */
    2.18  
    2.19    def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
    2.20 -    protocol_command_raw("Document.define_blob", Bytes(digest.toString), bytes)
    2.21 -
    2.22 -
    2.23 -  /* commands */
    2.24 +    protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
    2.25  
    2.26    def define_command(command: Command): Unit =
    2.27    {
     3.1 --- a/src/Pure/PIDE/prover.scala	Thu Apr 03 13:49:37 2014 +0200
     3.2 +++ b/src/Pure/PIDE/prover.scala	Thu Apr 03 14:54:17 2014 +0200
     3.3 @@ -56,3 +56,44 @@
     3.4    }
     3.5  }
     3.6  
     3.7 +trait Prover
     3.8 +{
     3.9 +  /* text and tree data */
    3.10 +
    3.11 +  def encode(s: String): String
    3.12 +  def decode(s: String): String
    3.13 +
    3.14 +  object Encode
    3.15 +  {
    3.16 +    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
    3.17 +  }
    3.18 +
    3.19 +  def xml_cache: XML.Cache
    3.20 +
    3.21 +
    3.22 +  /* process management */
    3.23 +
    3.24 +  def join(): Unit
    3.25 +  def terminate(): Unit
    3.26 +
    3.27 +  def protocol_command_bytes(name: String, args: Bytes*): Unit
    3.28 +  def protocol_command(name: String, args: String*): Unit
    3.29 +
    3.30 +
    3.31 +  /* PIDE protocol commands */
    3.32 +
    3.33 +  def options(opts: Options): Unit
    3.34 +
    3.35 +  def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit
    3.36 +  def define_command(command: Command): Unit
    3.37 +
    3.38 +  def discontinue_execution(): Unit
    3.39 +  def cancel_exec(id: Document_ID.Exec): Unit
    3.40 +
    3.41 +  def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
    3.42 +    edits: List[Document.Edit_Command]): Unit
    3.43 +  def remove_versions(versions: List[Document.Version]): Unit
    3.44 +
    3.45 +  def dialog_result(serial: Long, result: String): Unit
    3.46 +}
    3.47 +
     4.1 --- a/src/Pure/PIDE/resources.scala	Thu Apr 03 13:49:37 2014 +0200
     4.2 +++ b/src/Pure/PIDE/resources.scala	Thu Apr 03 14:54:17 2014 +0200
     4.3 @@ -101,5 +101,11 @@
     4.4      Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
     4.5  
     4.6    def commit(change: Session.Change) { }
     4.7 +
     4.8 +
     4.9 +  /* prover process */
    4.10 +
    4.11 +  def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
    4.12 +    new Isabelle_Process(receiver, args) with Protocol
    4.13  }
    4.14  
     5.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 03 13:49:37 2014 +0200
     5.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 03 14:54:17 2014 +0200
     5.3 @@ -51,8 +51,6 @@
     5.4  
     5.5    /* protocol handlers */
     5.6  
     5.7 -  type Prover = Isabelle_Process with Protocol
     5.8 -
     5.9    abstract class Protocol_Handler
    5.10    {
    5.11      def stop(prover: Prover): Unit = {}
    5.12 @@ -258,7 +256,7 @@
    5.13  
    5.14    /* actor messages */
    5.15  
    5.16 -  private case class Start(args: List[String])
    5.17 +  private case class Start(name: String, args: List[String])
    5.18    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    5.19    private case class Protocol_Command(name: String, args: List[String])
    5.20    private case class Messages(msgs: List[Prover.Message])
    5.21 @@ -307,7 +305,7 @@
    5.22        def cancel() { timer.cancel() }
    5.23      }
    5.24  
    5.25 -    var prover: Option[Session.Prover] = None
    5.26 +    var prover: Option[Prover] = None
    5.27  
    5.28  
    5.29      /* delayed command changes */
    5.30 @@ -505,10 +503,10 @@
    5.31        receiveWithin(delay_commands_changed.flush_timeout) {
    5.32          case TIMEOUT => delay_commands_changed.flush()
    5.33  
    5.34 -        case Start(args) if prover.isEmpty =>
    5.35 +        case Start(name, args) if prover.isEmpty =>
    5.36            if (phase == Session.Inactive || phase == Session.Failed) {
    5.37              phase = Session.Startup
    5.38 -            prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
    5.39 +            prover = Some(resources.start_prover(receiver.invoke _, name, args))
    5.40            }
    5.41  
    5.42          case Stop =>
    5.43 @@ -572,9 +570,9 @@
    5.44  
    5.45    /* actions */
    5.46  
    5.47 -  def start(args: List[String])
    5.48 +  def start(name: String, args: List[String])
    5.49    {
    5.50 -    session_actor ! Start(args)
    5.51 +    session_actor ! Start(name, args)
    5.52    }
    5.53  
    5.54    def stop()
     6.1 --- a/src/Pure/System/invoke_scala.scala	Thu Apr 03 13:49:37 2014 +0200
     6.2 +++ b/src/Pure/System/invoke_scala.scala	Thu Apr 03 14:54:17 2014 +0200
     6.3 @@ -72,24 +72,22 @@
     6.4  {
     6.5    private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
     6.6  
     6.7 -  private def fulfill(prover: Session.Prover,
     6.8 -    id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = synchronized
     6.9 -  {
    6.10 -    if (futures.isDefinedAt(id)) {
    6.11 -      prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
    6.12 -      futures -= id
    6.13 +  private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
    6.14 +    synchronized
    6.15 +    {
    6.16 +      if (futures.isDefinedAt(id)) {
    6.17 +        prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
    6.18 +        futures -= id
    6.19 +      }
    6.20      }
    6.21 -  }
    6.22  
    6.23 -  private def cancel(prover: Session.Prover,
    6.24 -    id: String, future: java.util.concurrent.Future[Unit])
    6.25 +  private def cancel(prover: Prover, id: String, future: java.util.concurrent.Future[Unit])
    6.26    {
    6.27      future.cancel(true)
    6.28      fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
    6.29    }
    6.30  
    6.31 -  private def invoke_scala(
    6.32 -    prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized
    6.33 +  private def invoke_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
    6.34    {
    6.35      msg.properties match {
    6.36        case Markup.Invoke_Scala(name, id) =>
    6.37 @@ -104,8 +102,7 @@
    6.38      }
    6.39    }
    6.40  
    6.41 -  private def cancel_scala(
    6.42 -    prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized
    6.43 +  private def cancel_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
    6.44    {
    6.45      msg.properties match {
    6.46        case Markup.Cancel_Scala(id) =>
    6.47 @@ -118,7 +115,7 @@
    6.48      }
    6.49    }
    6.50  
    6.51 -  override def stop(prover: Session.Prover): Unit = synchronized
    6.52 +  override def stop(prover: Prover): Unit = synchronized
    6.53    {
    6.54      for ((id, future) <- futures) cancel(prover, id, future)
    6.55      futures = Map.empty
     7.1 --- a/src/Pure/System/isabelle_process.scala	Thu Apr 03 13:49:37 2014 +0200
     7.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Apr 03 14:54:17 2014 +0200
     7.3 @@ -17,24 +17,19 @@
     7.4  
     7.5  
     7.6  class Isabelle_Process(
     7.7 -    receiver: Prover.Message => Unit = Console.println(_),
     7.8 -    arguments: List[String] = Nil)
     7.9 +  receiver: Prover.Message => Unit = Console.println(_),
    7.10 +  prover_args: List[String] = Nil)
    7.11  {
    7.12 -  /* text representation */
    7.13 +  /* text and tree data */
    7.14  
    7.15    def encode(s: String): String = Symbol.encode(s)
    7.16    def decode(s: String): String = Symbol.decode(s)
    7.17  
    7.18 -  object Encode
    7.19 -  {
    7.20 -    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
    7.21 -  }
    7.22 +  val xml_cache = new XML.Cache()
    7.23  
    7.24  
    7.25    /* output */
    7.26  
    7.27 -  val xml_cache = new XML.Cache()
    7.28 -
    7.29    private def system_output(text: String)
    7.30    {
    7.31      receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
    7.32 @@ -76,21 +71,21 @@
    7.33    @volatile private var command_input: (Thread, Actor) = null
    7.34  
    7.35  
    7.36 +
    7.37    /** process manager **/
    7.38  
    7.39 -  def command_line(channel: System_Channel, args: List[String]): List[String] =
    7.40 -    Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: (channel.isabelle_args ::: args)
    7.41 -
    7.42    private val system_channel = System_Channel()
    7.43  
    7.44    private val process =
    7.45      try {
    7.46 -      val cmdline = command_line(system_channel, arguments)
    7.47 +      val cmdline =
    7.48 +        Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
    7.49 +          (system_channel.isabelle_args ::: prover_args)
    7.50        new Isabelle_System.Managed_Process(null, null, false, cmdline: _*)
    7.51      }
    7.52      catch { case e: IOException => system_channel.accepted(); throw(e) }
    7.53  
    7.54 -  val (_, process_result) =
    7.55 +  private val (_, process_result) =
    7.56      Simple_Thread.future("process_result") { process.join }
    7.57  
    7.58    private def terminate_process()
    7.59 @@ -322,17 +317,15 @@
    7.60    }
    7.61  
    7.62  
    7.63 -  /** main methods **/
    7.64  
    7.65 -  def protocol_command_raw(name: String, args: Bytes*): Unit =
    7.66 +  /** protocol commands **/
    7.67 +
    7.68 +  def protocol_command_bytes(name: String, args: Bytes*): Unit =
    7.69      command_input._2 ! Input_Chunks(Bytes(name) :: args.toList)
    7.70  
    7.71    def protocol_command(name: String, args: String*)
    7.72    {
    7.73      receiver(new Prover.Input(name, args.toList))
    7.74 -    protocol_command_raw(name, args.map(Bytes(_)): _*)
    7.75 +    protocol_command_bytes(name, args.map(Bytes(_)): _*)
    7.76    }
    7.77 -
    7.78 -  def options(opts: Options): Unit =
    7.79 -    protocol_command("Isabelle_Process.options", YXML.string_of_body(opts.encode))
    7.80  }
     8.1 --- a/src/Pure/Tools/simplifier_trace.scala	Thu Apr 03 13:49:37 2014 +0200
     8.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Thu Apr 03 14:54:17 2014 +0200
     8.3 @@ -300,7 +300,7 @@
     8.4  
     8.5    class Handler extends Session.Protocol_Handler
     8.6    {
     8.7 -    private def cancel(prover: Session.Prover, msg: Prover.Protocol_Output): Boolean =
     8.8 +    private def cancel(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     8.9        msg.properties match {
    8.10          case Markup.Simp_Trace_Cancel(serial) =>
    8.11            manager ! Cancel(serial)
    8.12 @@ -309,7 +309,7 @@
    8.13            false
    8.14        }
    8.15  
    8.16 -    override def stop(prover: Session.Prover) =
    8.17 +    override def stop(prover: Prover) =
    8.18      {
    8.19        manager ! Clear_Memory
    8.20        manager ! Stop
     9.1 --- a/src/Pure/Tools/sledgehammer_params.scala	Thu Apr 03 13:49:37 2014 +0200
     9.2 +++ b/src/Pure/Tools/sledgehammer_params.scala	Thu Apr 03 14:54:17 2014 +0200
     9.3 @@ -36,8 +36,7 @@
     9.4      }
     9.5      def get_provers: String = synchronized { _provers }
     9.6  
     9.7 -    private def sledgehammer_provers(
     9.8 -      prover: Session.Prover, msg: Prover.Protocol_Output): Boolean =
     9.9 +    private def sledgehammer_provers(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    9.10      {
    9.11        update_provers(msg.text)
    9.12        true
    10.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Apr 03 13:49:37 2014 +0200
    10.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Apr 03 14:54:17 2014 +0200
    10.3 @@ -293,7 +293,7 @@
    10.4      if (PIDE.startup_failure.isEmpty) {
    10.5        message match {
    10.6          case msg: EditorStarted =>
    10.7 -          PIDE.session.start(Isabelle_Logic.session_args())
    10.8 +          PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
    10.9  
   10.10          case msg: BufferUpdate
   10.11          if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>