--- 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;
--- 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 =
{
--- 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
+}
+
--- 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
}
--- 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()
--- 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
--- 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))
}
--- 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
--- 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
--- 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 =>