src/Pure/System/isabelle_process.scala
changeset 57917 8ce97e5d545f
parent 57916 2c2c24dbf0a4
child 60215 5fb4990dfc73
--- 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)
+  }
+