diff -r 2c2c24dbf0a4 -r 8ce97e5d545f src/Pure/System/isabelle_process.scala --- 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) + } +