tuned signature;

--- a/src/Pure/PIDE/prover.scala	Tue Aug 12 18:36:43 2014 +0200
+++ b/src/Pure/PIDE/prover.scala	Tue Aug 12 18:54:53 2014 +0200
@@ -27,7 +27,6 @@
 
   trait System_Process
   {
-    def channel: System_Channel
     def stdout: BufferedReader
     def stderr: BufferedReader
     def terminate: Unit
@@ -85,6 +84,7 @@
 
 abstract class Prover(
   receiver: Prover.Message => Unit,
+  system_channel: System_Channel,
   system_process: Prover.System_Process) extends Protocol
 {
   /* output */
@@ -103,7 +103,7 @@
 
   private def output(kind: String, props: Properties.T, body: XML.Body)
   {
-    if (kind == Markup.INIT) system_process.channel.accepted()
+    if (kind == Markup.INIT) system_channel.accepted()
 
     val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
     val reports = Protocol.message_reports(props, body)
@@ -157,7 +157,7 @@
       exit_message(127)
     }
     else {
-      val (command_stream, message_stream) = system_process.channel.rendezvous()
+      val (command_stream, message_stream) = system_channel.rendezvous()
 
       command_input_init(command_stream)
       val stdout = physical_output(false)
@@ -171,7 +171,7 @@
       system_output("process_manager terminated")
       exit_message(rc)
     }
-    system_process.channel.accepted()
+    system_channel.accepted()
   }
 
 

--- a/src/Pure/PIDE/resources.scala	Tue Aug 12 18:36:43 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Aug 12 18:54:53 2014 +0200
@@ -126,6 +126,6 @@
   /* prover process */
 
   def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
-    new Isabelle_Process(receiver, args)
+    Isabelle_Process(receiver, args)
 }
 

--- a/src/Pure/System/isabelle_process.scala	Tue Aug 12 18:36:43 2014 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Aug 12 18:54:53 2014 +0200
@@ -7,25 +7,37 @@
 package isabelle
 
 
-class Isabelle_Process(
-  receiver: Prover.Message => Unit = Console.println(_),
-  prover_args: List[String] = Nil) extends Prover(receiver,
-    {
-      val system_channel = System_Channel()
+object Isabelle_Process
+{
+  def apply(
+    receiver: Prover.Message => Unit = Console.println(_),
+    prover_args: List[String] = Nil): Isabelle_Process =
+  {
+    val system_channel = System_Channel()
+    val system_process =
       try {
         val cmdline =
           Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
             (system_channel.prover_args ::: prover_args)
         val process =
           new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
-            Prover.System_Process { def channel = system_channel }
+            Prover.System_Process
         process.stdin.close
         process
       }
       catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) }
-    })
-{
-  def encode(s: String): String = Symbol.encode(s)
-  def decode(s: String): String = Symbol.decode(s)
+
+    new Isabelle_Process(receiver, system_channel, system_process)
+  }
 }
 
+class Isabelle_Process private(
+    receiver: Prover.Message => Unit,
+    system_channel: System_Channel,
+    system_process: Prover.System_Process)
+  extends Prover(receiver, system_channel, system_process)
+  {
+    def encode(s: String): String = Symbol.encode(s)
+    def decode(s: String): String = Symbol.decode(s)
+  }
+