# HG changeset patch # User wenzelm # Date 1407862493 -7200 # Node ID 8ce97e5d545f9b281e5c93360ab18e835b838bf7 # Parent 2c2c24dbf0a49c99d6679c1e8729469125842f88 tuned signature; diff -r 2c2c24dbf0a4 -r 8ce97e5d545f src/Pure/PIDE/prover.scala --- 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() } diff -r 2c2c24dbf0a4 -r 8ce97e5d545f src/Pure/PIDE/resources.scala --- 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) } 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) + } +