# HG changeset patch
# User wenzelm
# Date 1489869647 -3600
# Node ID c0fb8405416c38a3c078b113c14347c0590f71c0
# Parent  c7097ccbffb78eb4b8c238c8148b9ccb268f64dd
simplified signature (despite 448325de6e4f);

diff -r c7097ccbffb7 -r c0fb8405416c src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sat Mar 18 21:24:54 2017 +0100
+++ b/src/Pure/PIDE/prover.scala	Sat Mar 18 21:40:47 2017 +0100
@@ -13,17 +13,6 @@
 
 object Prover
 {
-  /* underlying system process */
-
-  trait System_Process
-  {
-    def stdout: BufferedReader
-    def stderr: BufferedReader
-    def terminate: Unit
-    def join: Int
-  }
-
-
   /* messages */
 
   sealed abstract class Message
@@ -76,8 +65,8 @@
 abstract class Prover(
   receiver: Prover.Receiver,
   xml_cache: XML.Cache,
-  system_channel: System_Channel,
-  system_process: Prover.System_Process) extends Protocol
+  channel: System_Channel,
+  process: Bash.Process) extends Protocol
 {
   /** receiver output **/
 
@@ -93,7 +82,7 @@
 
   private def output(kind: String, props: Properties.T, body: XML.Body)
   {
-    if (kind == Markup.INIT) system_channel.accepted()
+    if (kind == Markup.INIT) channel.accepted()
 
     val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
     val reports = Protocol_Message.reports(props, body)
@@ -110,11 +99,11 @@
   /** process manager **/
 
   private val process_result: Future[Int] =
-    Future.thread("process_result") { system_process.join }
+    Future.thread("process_result") { process.join }
 
   private def terminate_process()
   {
-    try { system_process.terminate }
+    try { process.terminate }
     catch {
       case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
     }
@@ -126,10 +115,10 @@
     {
       var finished: Option[Boolean] = None
       val result = new StringBuilder(100)
-      while (finished.isEmpty && (system_process.stderr.ready || !process_result.is_finished)) {
-        while (finished.isEmpty && system_process.stderr.ready) {
+      while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
+        while (finished.isEmpty && process.stderr.ready) {
           try {
-            val c = system_process.stderr.read
+            val c = process.stderr.read
             if (c == 2) finished = Some(true)
             else result += c.toChar
           }
@@ -147,7 +136,7 @@
       exit_message(127)
     }
     else {
-      val (command_stream, message_stream) = system_channel.rendezvous()
+      val (command_stream, message_stream) = channel.rendezvous()
 
       command_input_init(command_stream)
       val stdout = physical_output(false)
@@ -161,7 +150,7 @@
       system_output("process_manager terminated")
       exit_message(rc)
     }
-    system_channel.accepted()
+    channel.accepted()
   }
 
 
@@ -221,8 +210,8 @@
   private def physical_output(err: Boolean): Thread =
   {
     val (name, reader, markup) =
-      if (err) ("standard_error", system_process.stderr, Markup.STDERR)
-      else ("standard_output", system_process.stdout, Markup.STDOUT)
+      if (err) ("standard_error", process.stderr, Markup.STDERR)
+      else ("standard_output", process.stdout, Markup.STDOUT)
 
     Standard_Thread.fork(name) {
       try {
diff -r c7097ccbffb7 -r c0fb8405416c src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sat Mar 18 21:24:54 2017 +0100
+++ b/src/Pure/System/bash.scala	Sat Mar 18 21:40:47 2017 +0100
@@ -69,7 +69,6 @@
       env: Map[String, String],
       redirect: Boolean,
       cleanup: () => Unit)
-    extends Prover.System_Process
   {
     private val timing_file = Isabelle_System.tmp_file("bash_timing")
     private val timing = Synchronized[Option[Timing]](None)
diff -r c7097ccbffb7 -r c0fb8405416c src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Mar 18 21:24:54 2017 +0100
+++ b/src/Pure/System/isabelle_process.scala	Sat Mar 18 21:40:47 2017 +0100
@@ -63,7 +63,7 @@
     receiver: Prover.Receiver,
     xml_cache: XML.Cache,
     channel: System_Channel,
-    process: Prover.System_Process)
+    process: Bash.Process)
   extends Prover(receiver, xml_cache, channel, process)
 {
   def encode(s: String): String = Symbol.encode(s)