# HG changeset patch
# User wenzelm
# Date 1396529657 -7200
# Node ID d92eb5c3960db2da463e9c54753d9550d9211665
# Parent  fe520afb8041b5ba5939a82023722663eb1cb0f5
more general prover operations;

diff -r fe520afb8041 -r d92eb5c3960d src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Apr 03 14:54:17 2014 +0200
@@ -8,11 +8,11 @@
 struct
 
 val _ =
-  Isabelle_Process.protocol_command "Isabelle_Process.echo"
+  Isabelle_Process.protocol_command "Prover.echo"
     (fn args => List.app writeln args);
 
 val _ =
-  Isabelle_Process.protocol_command "Isabelle_Process.options"
+  Isabelle_Process.protocol_command "Prover.options"
     (fn [options_yxml] =>
       let val options = Options.decode (YXML.parse_body options_yxml) in
         Options.set_default options;
diff -r fe520afb8041 -r d92eb5c3960d src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Apr 03 14:54:17 2014 +0200
@@ -325,15 +325,18 @@
 }
 
 
-trait Protocol extends Isabelle_Process
+trait Protocol extends Prover
 {
-  /* inlined files */
+  /* options */
+
+  def options(opts: Options): Unit =
+    protocol_command("Prover.options", YXML.string_of_body(opts.encode))
+
+
+  /* interned items */
 
   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
-    protocol_command_raw("Document.define_blob", Bytes(digest.toString), bytes)
-
-
-  /* commands */
+    protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
 
   def define_command(command: Command): Unit =
   {
diff -r fe520afb8041 -r d92eb5c3960d src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Pure/PIDE/prover.scala	Thu Apr 03 14:54:17 2014 +0200
@@ -56,3 +56,44 @@
   }
 }
 
+trait Prover
+{
+  /* text and tree data */
+
+  def encode(s: String): String
+  def decode(s: String): String
+
+  object Encode
+  {
+    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
+  }
+
+  def xml_cache: XML.Cache
+
+
+  /* process management */
+
+  def join(): Unit
+  def terminate(): Unit
+
+  def protocol_command_bytes(name: String, args: Bytes*): Unit
+  def protocol_command(name: String, args: String*): Unit
+
+
+  /* PIDE protocol commands */
+
+  def options(opts: Options): Unit
+
+  def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit
+  def define_command(command: Command): Unit
+
+  def discontinue_execution(): Unit
+  def cancel_exec(id: Document_ID.Exec): Unit
+
+  def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
+    edits: List[Document.Edit_Command]): Unit
+  def remove_versions(versions: List[Document.Version]): Unit
+
+  def dialog_result(serial: Long, result: String): Unit
+}
+
diff -r fe520afb8041 -r d92eb5c3960d src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Apr 03 14:54:17 2014 +0200
@@ -101,5 +101,11 @@
     Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
 
   def commit(change: Session.Change) { }
+
+
+  /* prover process */
+
+  def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
+    new Isabelle_Process(receiver, args) with Protocol
 }
 
diff -r fe520afb8041 -r d92eb5c3960d src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Apr 03 14:54:17 2014 +0200
@@ -51,8 +51,6 @@
 
   /* protocol handlers */
 
-  type Prover = Isabelle_Process with Protocol
-
   abstract class Protocol_Handler
   {
     def stop(prover: Prover): Unit = {}
@@ -258,7 +256,7 @@
 
   /* actor messages */
 
-  private case class Start(args: List[String])
+  private case class Start(name: String, 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[Prover.Message])
@@ -307,7 +305,7 @@
       def cancel() { timer.cancel() }
     }
 
-    var prover: Option[Session.Prover] = None
+    var prover: Option[Prover] = None
 
 
     /* delayed command changes */
@@ -505,10 +503,10 @@
       receiveWithin(delay_commands_changed.flush_timeout) {
         case TIMEOUT => delay_commands_changed.flush()
 
-        case Start(args) if prover.isEmpty =>
+        case Start(name, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
-            prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
+            prover = Some(resources.start_prover(receiver.invoke _, name, args))
           }
 
         case Stop =>
@@ -572,9 +570,9 @@
 
   /* actions */
 
-  def start(args: List[String])
+  def start(name: String, args: List[String])
   {
-    session_actor ! Start(args)
+    session_actor ! Start(name, args)
   }
 
   def stop()
diff -r fe520afb8041 -r d92eb5c3960d src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Pure/System/invoke_scala.scala	Thu Apr 03 14:54:17 2014 +0200
@@ -72,24 +72,22 @@
 {
   private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
 
-  private def fulfill(prover: Session.Prover,
-    id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = synchronized
-  {
-    if (futures.isDefinedAt(id)) {
-      prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
-      futures -= id
+  private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
+    synchronized
+    {
+      if (futures.isDefinedAt(id)) {
+        prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
+        futures -= id
+      }
     }
-  }
 
-  private def cancel(prover: Session.Prover,
-    id: String, future: java.util.concurrent.Future[Unit])
+  private def cancel(prover: Prover, id: String, future: java.util.concurrent.Future[Unit])
   {
     future.cancel(true)
     fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
   }
 
-  private def invoke_scala(
-    prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized
+  private def invoke_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
   {
     msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
@@ -104,8 +102,7 @@
     }
   }
 
-  private def cancel_scala(
-    prover: Session.Prover, msg: Prover.Protocol_Output): Boolean = synchronized
+  private def cancel_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
   {
     msg.properties match {
       case Markup.Cancel_Scala(id) =>
@@ -118,7 +115,7 @@
     }
   }
 
-  override def stop(prover: Session.Prover): Unit = synchronized
+  override def stop(prover: Prover): Unit = synchronized
   {
     for ((id, future) <- futures) cancel(prover, id, future)
     futures = Map.empty
diff -r fe520afb8041 -r d92eb5c3960d src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Apr 03 14:54:17 2014 +0200
@@ -17,24 +17,19 @@
 
 
 class Isabelle_Process(
-    receiver: Prover.Message => Unit = Console.println(_),
-    arguments: List[String] = Nil)
+  receiver: Prover.Message => Unit = Console.println(_),
+  prover_args: List[String] = Nil)
 {
-  /* text representation */
+  /* text and tree data */
 
   def encode(s: String): String = Symbol.encode(s)
   def decode(s: String): String = Symbol.decode(s)
 
-  object Encode
-  {
-    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
-  }
+  val xml_cache = new XML.Cache()
 
 
   /* output */
 
-  val xml_cache = new XML.Cache()
-
   private def system_output(text: String)
   {
     receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
@@ -76,21 +71,21 @@
   @volatile private var command_input: (Thread, Actor) = null
 
 
+
   /** process manager **/
 
-  def command_line(channel: System_Channel, args: List[String]): List[String] =
-    Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: (channel.isabelle_args ::: args)
-
   private val system_channel = System_Channel()
 
   private val process =
     try {
-      val cmdline = command_line(system_channel, arguments)
+      val cmdline =
+        Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
+          (system_channel.isabelle_args ::: prover_args)
       new Isabelle_System.Managed_Process(null, null, false, cmdline: _*)
     }
     catch { case e: IOException => system_channel.accepted(); throw(e) }
 
-  val (_, process_result) =
+  private val (_, process_result) =
     Simple_Thread.future("process_result") { process.join }
 
   private def terminate_process()
@@ -322,17 +317,15 @@
   }
 
 
-  /** main methods **/
 
-  def protocol_command_raw(name: String, args: Bytes*): Unit =
+  /** protocol commands **/
+
+  def protocol_command_bytes(name: String, args: Bytes*): Unit =
     command_input._2 ! Input_Chunks(Bytes(name) :: args.toList)
 
   def protocol_command(name: String, args: String*)
   {
     receiver(new Prover.Input(name, args.toList))
-    protocol_command_raw(name, args.map(Bytes(_)): _*)
+    protocol_command_bytes(name, args.map(Bytes(_)): _*)
   }
-
-  def options(opts: Options): Unit =
-    protocol_command("Isabelle_Process.options", YXML.string_of_body(opts.encode))
 }
diff -r fe520afb8041 -r d92eb5c3960d src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Thu Apr 03 14:54:17 2014 +0200
@@ -300,7 +300,7 @@
 
   class Handler extends Session.Protocol_Handler
   {
-    private def cancel(prover: Session.Prover, msg: Prover.Protocol_Output): Boolean =
+    private def cancel(prover: Prover, msg: Prover.Protocol_Output): Boolean =
       msg.properties match {
         case Markup.Simp_Trace_Cancel(serial) =>
           manager ! Cancel(serial)
@@ -309,7 +309,7 @@
           false
       }
 
-    override def stop(prover: Session.Prover) =
+    override def stop(prover: Prover) =
     {
       manager ! Clear_Memory
       manager ! Stop
diff -r fe520afb8041 -r d92eb5c3960d src/Pure/Tools/sledgehammer_params.scala
--- a/src/Pure/Tools/sledgehammer_params.scala	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Pure/Tools/sledgehammer_params.scala	Thu Apr 03 14:54:17 2014 +0200
@@ -36,8 +36,7 @@
     }
     def get_provers: String = synchronized { _provers }
 
-    private def sledgehammer_provers(
-      prover: Session.Prover, msg: Prover.Protocol_Output): Boolean =
+    private def sledgehammer_provers(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     {
       update_provers(msg.text)
       true
diff -r fe520afb8041 -r d92eb5c3960d src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Apr 03 13:49:37 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Apr 03 14:54:17 2014 +0200
@@ -293,7 +293,7 @@
     if (PIDE.startup_failure.isEmpty) {
       message match {
         case msg: EditorStarted =>
-          PIDE.session.start(Isabelle_Logic.session_args())
+          PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
 
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>