simplified signature (despite 448325de6e4f);
authorwenzelm
Sat Mar 18 21:40:47 2017 +0100 (2017-03-18)
changeset 65316c0fb8405416c
parent 65315 c7097ccbffb7
child 65317 b9f5cd845616
simplified signature (despite 448325de6e4f);
src/Pure/PIDE/prover.scala
src/Pure/System/bash.scala
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/PIDE/prover.scala	Sat Mar 18 21:24:54 2017 +0100
     1.2 +++ b/src/Pure/PIDE/prover.scala	Sat Mar 18 21:40:47 2017 +0100
     1.3 @@ -13,17 +13,6 @@
     1.4  
     1.5  object Prover
     1.6  {
     1.7 -  /* underlying system process */
     1.8 -
     1.9 -  trait System_Process
    1.10 -  {
    1.11 -    def stdout: BufferedReader
    1.12 -    def stderr: BufferedReader
    1.13 -    def terminate: Unit
    1.14 -    def join: Int
    1.15 -  }
    1.16 -
    1.17 -
    1.18    /* messages */
    1.19  
    1.20    sealed abstract class Message
    1.21 @@ -76,8 +65,8 @@
    1.22  abstract class Prover(
    1.23    receiver: Prover.Receiver,
    1.24    xml_cache: XML.Cache,
    1.25 -  system_channel: System_Channel,
    1.26 -  system_process: Prover.System_Process) extends Protocol
    1.27 +  channel: System_Channel,
    1.28 +  process: Bash.Process) extends Protocol
    1.29  {
    1.30    /** receiver output **/
    1.31  
    1.32 @@ -93,7 +82,7 @@
    1.33  
    1.34    private def output(kind: String, props: Properties.T, body: XML.Body)
    1.35    {
    1.36 -    if (kind == Markup.INIT) system_channel.accepted()
    1.37 +    if (kind == Markup.INIT) channel.accepted()
    1.38  
    1.39      val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
    1.40      val reports = Protocol_Message.reports(props, body)
    1.41 @@ -110,11 +99,11 @@
    1.42    /** process manager **/
    1.43  
    1.44    private val process_result: Future[Int] =
    1.45 -    Future.thread("process_result") { system_process.join }
    1.46 +    Future.thread("process_result") { process.join }
    1.47  
    1.48    private def terminate_process()
    1.49    {
    1.50 -    try { system_process.terminate }
    1.51 +    try { process.terminate }
    1.52      catch {
    1.53        case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
    1.54      }
    1.55 @@ -126,10 +115,10 @@
    1.56      {
    1.57        var finished: Option[Boolean] = None
    1.58        val result = new StringBuilder(100)
    1.59 -      while (finished.isEmpty && (system_process.stderr.ready || !process_result.is_finished)) {
    1.60 -        while (finished.isEmpty && system_process.stderr.ready) {
    1.61 +      while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
    1.62 +        while (finished.isEmpty && process.stderr.ready) {
    1.63            try {
    1.64 -            val c = system_process.stderr.read
    1.65 +            val c = process.stderr.read
    1.66              if (c == 2) finished = Some(true)
    1.67              else result += c.toChar
    1.68            }
    1.69 @@ -147,7 +136,7 @@
    1.70        exit_message(127)
    1.71      }
    1.72      else {
    1.73 -      val (command_stream, message_stream) = system_channel.rendezvous()
    1.74 +      val (command_stream, message_stream) = channel.rendezvous()
    1.75  
    1.76        command_input_init(command_stream)
    1.77        val stdout = physical_output(false)
    1.78 @@ -161,7 +150,7 @@
    1.79        system_output("process_manager terminated")
    1.80        exit_message(rc)
    1.81      }
    1.82 -    system_channel.accepted()
    1.83 +    channel.accepted()
    1.84    }
    1.85  
    1.86  
    1.87 @@ -221,8 +210,8 @@
    1.88    private def physical_output(err: Boolean): Thread =
    1.89    {
    1.90      val (name, reader, markup) =
    1.91 -      if (err) ("standard_error", system_process.stderr, Markup.STDERR)
    1.92 -      else ("standard_output", system_process.stdout, Markup.STDOUT)
    1.93 +      if (err) ("standard_error", process.stderr, Markup.STDERR)
    1.94 +      else ("standard_output", process.stdout, Markup.STDOUT)
    1.95  
    1.96      Standard_Thread.fork(name) {
    1.97        try {
     2.1 --- a/src/Pure/System/bash.scala	Sat Mar 18 21:24:54 2017 +0100
     2.2 +++ b/src/Pure/System/bash.scala	Sat Mar 18 21:40:47 2017 +0100
     2.3 @@ -69,7 +69,6 @@
     2.4        env: Map[String, String],
     2.5        redirect: Boolean,
     2.6        cleanup: () => Unit)
     2.7 -    extends Prover.System_Process
     2.8    {
     2.9      private val timing_file = Isabelle_System.tmp_file("bash_timing")
    2.10      private val timing = Synchronized[Option[Timing]](None)
     3.1 --- a/src/Pure/System/isabelle_process.scala	Sat Mar 18 21:24:54 2017 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Mar 18 21:40:47 2017 +0100
     3.3 @@ -63,7 +63,7 @@
     3.4      receiver: Prover.Receiver,
     3.5      xml_cache: XML.Cache,
     3.6      channel: System_Channel,
     3.7 -    process: Prover.System_Process)
     3.8 +    process: Bash.Process)
     3.9    extends Prover(receiver, xml_cache, channel, process)
    3.10  {
    3.11    def encode(s: String): String = Symbol.encode(s)