1.1 --- a/src/Pure/System/isabelle_process.scala	Wed Sep 21 17:50:25 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Sep 21 20:35:50 2011 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4  
     1.5    private def put_result(kind: String, props: Properties.T, body: XML.Body)
     1.6    {
     1.7 -    if (kind == Markup.INIT) rm_fifos()
     1.8 +    if (kind == Markup.INIT) system_channel.accepted()
     1.9      if (kind == Markup.RAW)
    1.10        receiver(new Result(XML.Elem(Markup(kind, props), body)))
    1.11      else {
    1.12 @@ -131,18 +131,16 @@
    1.13  
    1.14    /** process manager **/
    1.15  
    1.16 -  private val in_fifo = Isabelle_System.mk_fifo()
    1.17 -  private val out_fifo = Isabelle_System.mk_fifo()
    1.18 -  private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) }
    1.19 +  private val system_channel = System_Channel()
    1.20  
    1.21    private val process =
    1.22      try {
    1.23        val cmdline =
    1.24 -        List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W",
    1.25 -          in_fifo + ":" + out_fifo) ++ args
    1.26 +        Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
    1.27 +          (system_channel.isabelle_args ::: args.toList)
    1.28        new Isabelle_System.Managed_Process(true, cmdline: _*)
    1.29      }
    1.30 -    catch { case e: IOException => rm_fifos(); throw(e) }
    1.31 +    catch { case e: IOException => system_channel.accepted(); throw(e) }
    1.32  
    1.33    val process_result =
    1.34      Simple_Thread.future("process_result") { process.join }
    1.35 @@ -182,9 +180,7 @@
    1.36        process_result.join
    1.37      }
    1.38      else {
    1.39 -      // rendezvous
    1.40 -      val command_stream = Isabelle_System.fifo_output_stream(in_fifo)
    1.41 -      val message_stream = Isabelle_System.fifo_input_stream(out_fifo)
    1.42 +      val (command_stream, message_stream) = system_channel.rendezvous()
    1.43  
    1.44        standard_input = stdin_actor()
    1.45        val stdout = stdout_actor()
    1.46 @@ -197,7 +193,7 @@
    1.47        system_result("process_manager terminated")
    1.48        put_result(Markup.EXIT, "Return code: " + rc.toString)
    1.49      }
    1.50 -    rm_fifos()
    1.51 +    system_channel.accepted()
    1.52    }
    1.53  
    1.54  

     2.1 --- a/src/Pure/System/isabelle_system.scala	Wed Sep 21 17:50:25 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Wed Sep 21 20:35:50 2011 +0200
     2.3 @@ -10,8 +10,8 @@
     2.4  import java.lang.System
     2.5  import java.util.regex.Pattern
     2.6  import java.util.Locale
     2.7 -import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
     2.8 -  BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter, IOException}
     2.9 +import java.io.{InputStream, OutputStream, File, BufferedReader, InputStreamReader,
    2.10 +  BufferedWriter, OutputStreamWriter, IOException}
    2.11  import java.awt.{GraphicsEnvironment, Font}
    2.12  import java.awt.font.TextAttribute
    2.13  
    2.14 @@ -108,7 +108,7 @@
    2.15    def standard_path(path: Path): String = path.expand.implode
    2.16  
    2.17    def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
    2.18 -  def platform_file(path: Path) = new File(platform_path(path))
    2.19 +  def platform_file(path: Path): File = new File(platform_path(path))
    2.20  
    2.21    def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
    2.22  
    2.23 @@ -266,54 +266,6 @@
    2.24    }
    2.25  
    2.26  
    2.27 -  /* named pipes */
    2.28 -
    2.29 -  private val next_fifo = new Counter
    2.30 -
    2.31 -  def mk_fifo(): String =
    2.32 -  {
    2.33 -    val i = next_fifo()
    2.34 -    val script =
    2.35 -      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
    2.36 -      "echo -n \"$FIFO\"\n" +
    2.37 -      "mkfifo -m 600 \"$FIFO\"\n"
    2.38 -    val (out, err, rc) = bash(script)
    2.39 -    if (rc == 0) out else error(err.trim)
    2.40 -  }
    2.41 -
    2.42 -  def rm_fifo(fifo: String): Boolean =
    2.43 -    (new File(standard_system.jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
    2.44 -
    2.45 -  def fifo_input_stream(fifo: String): InputStream =
    2.46 -  {
    2.47 -    if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
    2.48 -      val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
    2.49 -      proc.getOutputStream.close
    2.50 -      proc.getErrorStream.close
    2.51 -      proc.getInputStream
    2.52 -    }
    2.53 -    else new FileInputStream(fifo)
    2.54 -  }
    2.55 -
    2.56 -  def fifo_output_stream(fifo: String): OutputStream =
    2.57 -  {
    2.58 -    if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
    2.59 -      val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
    2.60 -      proc.getInputStream.close
    2.61 -      proc.getErrorStream.close
    2.62 -      val out = proc.getOutputStream
    2.63 -      new OutputStream {
    2.64 -        override def close() { out.close(); proc.waitFor() }
    2.65 -        override def flush() { out.flush() }
    2.66 -        override def write(b: Array[Byte]) { out.write(b) }
    2.67 -        override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
    2.68 -        override def write(b: Int) { out.write(b) }
    2.69 -      }
    2.70 -    }
    2.71 -    else new FileOutputStream(fifo)
    2.72 -  }
    2.73 -
    2.74 -
    2.75  
    2.76    /** Isabelle resources **/
    2.77  

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/System/system_channel.scala	Wed Sep 21 20:35:50 2011 +0200
     3.3 @@ -0,0 +1,100 @@
     3.4 +/*  Title:      Pure/System/system_channel.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Portable system channel for inter-process communication.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
    3.14 +
    3.15 +
    3.16 +object System_Channel
    3.17 +{
    3.18 +  def apply(): System_Channel = new Fifo_Channel
    3.19 +}
    3.20 +
    3.21 +abstract class System_Channel
    3.22 +{
    3.23 +  def isabelle_args: List[String]
    3.24 +  def rendezvous(): (OutputStream, InputStream)
    3.25 +  def accepted(): Unit
    3.26 +}
    3.27 +
    3.28 +
    3.29 +object Fifo_Channel
    3.30 +{
    3.31 +  private val next_fifo = new Counter
    3.32 +}
    3.33 +
    3.34 +class Fifo_Channel extends System_Channel
    3.35 +{
    3.36 +  /* operations on named pipes */
    3.37 +
    3.38 +  private def mk_fifo(): String =
    3.39 +  {
    3.40 +    val i = Fifo_Channel.next_fifo()
    3.41 +    val script =
    3.42 +      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
    3.43 +      "echo -n \"$FIFO\"\n" +
    3.44 +      "mkfifo -m 600 \"$FIFO\"\n"
    3.45 +    val (out, err, rc) = Isabelle_System.bash(script)
    3.46 +    if (rc == 0) out else error(err.trim)
    3.47 +  }
    3.48 +
    3.49 +  private def rm_fifo(fifo: String): Boolean =
    3.50 +    Isabelle_System.platform_file(
    3.51 +      Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).delete
    3.52 +
    3.53 +  private def fifo_input_stream(fifo: String): InputStream =
    3.54 +  {
    3.55 +    if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
    3.56 +      val proc =
    3.57 +        Isabelle_System.execute(false,
    3.58 +          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
    3.59 +      proc.getOutputStream.close
    3.60 +      proc.getErrorStream.close
    3.61 +      proc.getInputStream
    3.62 +    }
    3.63 +    else new FileInputStream(fifo)
    3.64 +  }
    3.65 +
    3.66 +  private def fifo_output_stream(fifo: String): OutputStream =
    3.67 +  {
    3.68 +    if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
    3.69 +      val proc =
    3.70 +        Isabelle_System.execute(false,
    3.71 +          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
    3.72 +      proc.getInputStream.close
    3.73 +      proc.getErrorStream.close
    3.74 +      val out = proc.getOutputStream
    3.75 +      new OutputStream {
    3.76 +        override def close() { out.close(); proc.waitFor() }
    3.77 +        override def flush() { out.flush() }
    3.78 +        override def write(b: Array[Byte]) { out.write(b) }
    3.79 +        override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
    3.80 +        override def write(b: Int) { out.write(b) }
    3.81 +      }
    3.82 +    }
    3.83 +    else new FileOutputStream(fifo)
    3.84 +  }
    3.85 +
    3.86 +
    3.87 +  /* initialization */
    3.88 +
    3.89 +  private val fifo1 = mk_fifo()
    3.90 +  private val fifo2 = mk_fifo()
    3.91 +
    3.92 +  val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
    3.93 +
    3.94 +  def rendezvous(): (OutputStream, InputStream) =
    3.95 +  {
    3.96 +    /*rendezvous*/
    3.97 +    val output_stream = fifo_output_stream(fifo1)
    3.98 +    val input_stream = fifo_input_stream(fifo2)
    3.99 +    (output_stream, input_stream)
   3.100 +  }
   3.101 +
   3.102 +  def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
   3.103 +}

     4.1 --- a/src/Pure/build-jars	Wed Sep 21 17:50:25 2011 +0200
     4.2 +++ b/src/Pure/build-jars	Wed Sep 21 20:35:50 2011 +0200
     4.3 @@ -49,6 +49,7 @@
     4.4    System/session_manager.scala
     4.5    System/standard_system.scala
     4.6    System/swing_thread.scala
     4.7 +  System/system_channel.scala
     4.8    Thy/completion.scala
     4.9    Thy/html.scala
    4.10    Thy/thy_header.scala