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