src/Pure/System/system_channel.scala
author wenzelm
Fri Jul 20 22:29:25 2012 +0200 (2012-07-20)
changeset 48409 0d2114eb412a
parent 48373 527e2bad7cca
child 49695 8f61d1c7dded
permissions -rw-r--r--
more explicit java.io.{File => JFile};
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@48409
    11
import java.io.{InputStream, OutputStream, File => JFile, FileInputStream,
wenzelm@48409
    12
  FileOutputStream, IOException}
wenzelm@45028
    13
import java.net.{ServerSocket, InetAddress}
wenzelm@45027
    14
wenzelm@45027
    15
wenzelm@45027
    16
object System_Channel
wenzelm@45027
    17
{
wenzelm@45055
    18
  def apply(use_socket: Boolean = false): System_Channel =
wenzelm@45158
    19
    if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
wenzelm@45027
    20
}
wenzelm@45027
    21
wenzelm@45027
    22
abstract class System_Channel
wenzelm@45027
    23
{
wenzelm@45027
    24
  def isabelle_args: List[String]
wenzelm@45027
    25
  def rendezvous(): (OutputStream, InputStream)
wenzelm@45027
    26
  def accepted(): Unit
wenzelm@45027
    27
}
wenzelm@45027
    28
wenzelm@45027
    29
wenzelm@45028
    30
/** named pipes **/
wenzelm@45028
    31
wenzelm@45251
    32
private object Fifo_Channel
wenzelm@45027
    33
{
wenzelm@45243
    34
  private val next_fifo = Counter()
wenzelm@45027
    35
}
wenzelm@45027
    36
wenzelm@45251
    37
private class Fifo_Channel extends System_Channel
wenzelm@45027
    38
{
wenzelm@45027
    39
  private def mk_fifo(): String =
wenzelm@45027
    40
  {
wenzelm@45027
    41
    val i = Fifo_Channel.next_fifo()
wenzelm@45027
    42
    val script =
wenzelm@45027
    43
      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
wenzelm@45027
    44
      "echo -n \"$FIFO\"\n" +
wenzelm@45027
    45
      "mkfifo -m 600 \"$FIFO\"\n"
wenzelm@45027
    46
    val (out, err, rc) = Isabelle_System.bash(script)
wenzelm@45027
    47
    if (rc == 0) out else error(err.trim)
wenzelm@45027
    48
  }
wenzelm@45027
    49
wenzelm@45027
    50
  private def rm_fifo(fifo: String): Boolean =
wenzelm@48373
    51
    Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo).file.delete
wenzelm@45027
    52
wenzelm@45027
    53
  private def fifo_input_stream(fifo: String): InputStream =
wenzelm@45027
    54
  {
wenzelm@45158
    55
    require(!Platform.is_windows)
wenzelm@45158
    56
    new FileInputStream(fifo)
wenzelm@45027
    57
  }
wenzelm@45027
    58
wenzelm@45027
    59
  private def fifo_output_stream(fifo: String): OutputStream =
wenzelm@45027
    60
  {
wenzelm@45158
    61
    require(!Platform.is_windows)
wenzelm@45158
    62
    new FileOutputStream(fifo)
wenzelm@45027
    63
  }
wenzelm@45027
    64
wenzelm@45027
    65
wenzelm@45027
    66
  private val fifo1 = mk_fifo()
wenzelm@45027
    67
  private val fifo2 = mk_fifo()
wenzelm@45027
    68
wenzelm@45027
    69
  val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
wenzelm@45027
    70
wenzelm@45027
    71
  def rendezvous(): (OutputStream, InputStream) =
wenzelm@45027
    72
  {
wenzelm@45027
    73
    val output_stream = fifo_output_stream(fifo1)
wenzelm@45027
    74
    val input_stream = fifo_input_stream(fifo2)
wenzelm@45027
    75
    (output_stream, input_stream)
wenzelm@45027
    76
  }
wenzelm@45027
    77
wenzelm@45027
    78
  def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
wenzelm@45027
    79
}
wenzelm@45028
    80
wenzelm@45028
    81
wenzelm@45028
    82
/** sockets **/
wenzelm@45028
    83
wenzelm@45251
    84
private class Socket_Channel extends System_Channel
wenzelm@45028
    85
{
wenzelm@45028
    86
  private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
wenzelm@45028
    87
wenzelm@45028
    88
  def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
wenzelm@45028
    89
wenzelm@45028
    90
  def rendezvous(): (OutputStream, InputStream) =
wenzelm@45028
    91
  {
wenzelm@45028
    92
    val socket = server.accept
wenzelm@45028
    93
    (socket.getOutputStream, socket.getInputStream)
wenzelm@45028
    94
  }
wenzelm@45028
    95
wenzelm@45028
    96
  def accepted() { server.close }
wenzelm@45028
    97
}