src/Pure/System/system_channel.scala
author wenzelm
Wed, 21 Sep 2011 20:35:50 +0200
changeset 45027 f459e93a038e
child 45028 d608dd8cd409
permissions -rw-r--r--
more abstract wrapping of fifos as System_Channel;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/system_channel.scala
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     3
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     4
Portable system channel for inter-process communication.
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     5
*/
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     6
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     7
package isabelle
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     8
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     9
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    10
import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    11
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    12
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    13
object System_Channel
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    14
{
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    15
  def apply(): System_Channel = new Fifo_Channel
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    16
}
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    17
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    18
abstract class System_Channel
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    19
{
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    20
  def isabelle_args: List[String]
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    21
  def rendezvous(): (OutputStream, InputStream)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    22
  def accepted(): Unit
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    23
}
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    24
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    25
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    26
object Fifo_Channel
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    27
{
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    28
  private val next_fifo = new Counter
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    29
}
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    30
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    31
class Fifo_Channel extends System_Channel
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    32
{
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    33
  /* operations on named pipes */
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    34
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    35
  private def mk_fifo(): String =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    36
  {
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    37
    val i = Fifo_Channel.next_fifo()
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    38
    val script =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    39
      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    40
      "echo -n \"$FIFO\"\n" +
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    41
      "mkfifo -m 600 \"$FIFO\"\n"
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    42
    val (out, err, rc) = Isabelle_System.bash(script)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    43
    if (rc == 0) out else error(err.trim)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    44
  }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    45
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    46
  private def rm_fifo(fifo: String): Boolean =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    47
    Isabelle_System.platform_file(
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    48
      Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).delete
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    49
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    50
  private def fifo_input_stream(fifo: String): InputStream =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    51
  {
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    52
    if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    53
      val proc =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    54
        Isabelle_System.execute(false,
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    55
          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    56
      proc.getOutputStream.close
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    57
      proc.getErrorStream.close
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    58
      proc.getInputStream
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    59
    }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    60
    else new FileInputStream(fifo)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    61
  }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    62
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    63
  private def fifo_output_stream(fifo: String): OutputStream =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    64
  {
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    65
    if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    66
      val proc =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    67
        Isabelle_System.execute(false,
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    68
          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    69
      proc.getInputStream.close
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    70
      proc.getErrorStream.close
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    71
      val out = proc.getOutputStream
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    72
      new OutputStream {
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    73
        override def close() { out.close(); proc.waitFor() }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    74
        override def flush() { out.flush() }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    75
        override def write(b: Array[Byte]) { out.write(b) }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    76
        override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    77
        override def write(b: Int) { out.write(b) }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    78
      }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    79
    }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    80
    else new FileOutputStream(fifo)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    81
  }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    82
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    83
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    84
  /* initialization */
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    85
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    86
  private val fifo1 = mk_fifo()
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    87
  private val fifo2 = mk_fifo()
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    88
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    89
  val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    90
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    91
  def rendezvous(): (OutputStream, InputStream) =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    92
  {
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    93
    /*rendezvous*/
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    94
    val output_stream = fifo_output_stream(fifo1)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    95
    val input_stream = fifo_input_stream(fifo2)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    96
    (output_stream, input_stream)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    97
  }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    98
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    99
  def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
   100
}