# HG changeset patch # User wenzelm # Date 1316630150 -7200 # Node ID f459e93a038eded0022ca8ba7eb112afdb66d926 # Parent 5c0b0d67f9b15142ffe72ccf22e61efa02e0fb5c more abstract wrapping of fifos as System_Channel; diff -r 5c0b0d67f9b1 -r f459e93a038e src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Wed Sep 21 17:50:25 2011 +0200 +++ b/src/Pure/System/isabelle_process.scala Wed Sep 21 20:35:50 2011 +0200 @@ -96,7 +96,7 @@ private def put_result(kind: String, props: Properties.T, body: XML.Body) { - if (kind == Markup.INIT) rm_fifos() + if (kind == Markup.INIT) system_channel.accepted() if (kind == Markup.RAW) receiver(new Result(XML.Elem(Markup(kind, props), body))) else { @@ -131,18 +131,16 @@ /** process manager **/ - private val in_fifo = Isabelle_System.mk_fifo() - private val out_fifo = Isabelle_System.mk_fifo() - private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) } + private val system_channel = System_Channel() private val process = try { val cmdline = - List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W", - in_fifo + ":" + out_fifo) ++ args + Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: + (system_channel.isabelle_args ::: args.toList) new Isabelle_System.Managed_Process(true, cmdline: _*) } - catch { case e: IOException => rm_fifos(); throw(e) } + catch { case e: IOException => system_channel.accepted(); throw(e) } val process_result = Simple_Thread.future("process_result") { process.join } @@ -182,9 +180,7 @@ process_result.join } else { - // rendezvous - val command_stream = Isabelle_System.fifo_output_stream(in_fifo) - val message_stream = Isabelle_System.fifo_input_stream(out_fifo) + val (command_stream, message_stream) = system_channel.rendezvous() standard_input = stdin_actor() val stdout = stdout_actor() @@ -197,7 +193,7 @@ system_result("process_manager terminated") put_result(Markup.EXIT, "Return code: " + rc.toString) } - rm_fifos() + system_channel.accepted() } diff -r 5c0b0d67f9b1 -r f459e93a038e src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Wed Sep 21 17:50:25 2011 +0200 +++ b/src/Pure/System/isabelle_system.scala Wed Sep 21 20:35:50 2011 +0200 @@ -10,8 +10,8 @@ import java.lang.System import java.util.regex.Pattern import java.util.Locale -import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File, - BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter, IOException} +import java.io.{InputStream, OutputStream, File, BufferedReader, InputStreamReader, + BufferedWriter, OutputStreamWriter, IOException} import java.awt.{GraphicsEnvironment, Font} import java.awt.font.TextAttribute @@ -108,7 +108,7 @@ def standard_path(path: Path): String = path.expand.implode def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path)) - def platform_file(path: Path) = new File(platform_path(path)) + def platform_file(path: Path): File = new File(platform_path(path)) def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path) @@ -266,54 +266,6 @@ } - /* named pipes */ - - private val next_fifo = new Counter - - def mk_fifo(): String = - { - val i = next_fifo() - val script = - "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" + - "echo -n \"$FIFO\"\n" + - "mkfifo -m 600 \"$FIFO\"\n" - val (out, err, rc) = bash(script) - if (rc == 0) out else error(err.trim) - } - - def rm_fifo(fifo: String): Boolean = - (new File(standard_system.jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete - - def fifo_input_stream(fifo: String): InputStream = - { - if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream - val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-") - proc.getOutputStream.close - proc.getErrorStream.close - proc.getInputStream - } - else new FileInputStream(fifo) - } - - def fifo_output_stream(fifo: String): OutputStream = - { - if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream - val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo) - proc.getInputStream.close - proc.getErrorStream.close - val out = proc.getOutputStream - new OutputStream { - override def close() { out.close(); proc.waitFor() } - override def flush() { out.flush() } - override def write(b: Array[Byte]) { out.write(b) } - override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) } - override def write(b: Int) { out.write(b) } - } - } - else new FileOutputStream(fifo) - } - - /** Isabelle resources **/ diff -r 5c0b0d67f9b1 -r f459e93a038e src/Pure/System/system_channel.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/system_channel.scala Wed Sep 21 20:35:50 2011 +0200 @@ -0,0 +1,100 @@ +/* Title: Pure/System/system_channel.scala + Author: Makarius + +Portable system channel for inter-process communication. +*/ + +package isabelle + + +import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException} + + +object System_Channel +{ + def apply(): System_Channel = new Fifo_Channel +} + +abstract class System_Channel +{ + def isabelle_args: List[String] + def rendezvous(): (OutputStream, InputStream) + def accepted(): Unit +} + + +object Fifo_Channel +{ + private val next_fifo = new Counter +} + +class Fifo_Channel extends System_Channel +{ + /* operations on named pipes */ + + private def mk_fifo(): String = + { + val i = Fifo_Channel.next_fifo() + val script = + "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" + + "echo -n \"$FIFO\"\n" + + "mkfifo -m 600 \"$FIFO\"\n" + val (out, err, rc) = Isabelle_System.bash(script) + if (rc == 0) out else error(err.trim) + } + + private def rm_fifo(fifo: String): Boolean = + Isabelle_System.platform_file( + Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).delete + + private def fifo_input_stream(fifo: String): InputStream = + { + if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream + val proc = + Isabelle_System.execute(false, + Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-") + proc.getOutputStream.close + proc.getErrorStream.close + proc.getInputStream + } + else new FileInputStream(fifo) + } + + private def fifo_output_stream(fifo: String): OutputStream = + { + if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream + val proc = + Isabelle_System.execute(false, + Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo) + proc.getInputStream.close + proc.getErrorStream.close + val out = proc.getOutputStream + new OutputStream { + override def close() { out.close(); proc.waitFor() } + override def flush() { out.flush() } + override def write(b: Array[Byte]) { out.write(b) } + override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) } + override def write(b: Int) { out.write(b) } + } + } + else new FileOutputStream(fifo) + } + + + /* initialization */ + + private val fifo1 = mk_fifo() + private val fifo2 = mk_fifo() + + val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2) + + def rendezvous(): (OutputStream, InputStream) = + { + /*rendezvous*/ + val output_stream = fifo_output_stream(fifo1) + val input_stream = fifo_input_stream(fifo2) + (output_stream, input_stream) + } + + def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) } +} diff -r 5c0b0d67f9b1 -r f459e93a038e src/Pure/build-jars --- a/src/Pure/build-jars Wed Sep 21 17:50:25 2011 +0200 +++ b/src/Pure/build-jars Wed Sep 21 20:35:50 2011 +0200 @@ -49,6 +49,7 @@ System/session_manager.scala System/standard_system.scala System/swing_thread.scala + System/system_channel.scala Thy/completion.scala Thy/html.scala Thy/thy_header.scala