--- 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)
+ }
+