src/Pure/System/system_channel.scala
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 52537 4b5941730bd8
child 54005 132640f4c453
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
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@52537
    34
  private val next_fifo = Counter.make()
wenzelm@45027
    35
}
wenzelm@45027
    36
wenzelm@45251
    37
private class Fifo_Channel extends System_Channel
wenzelm@45027
    38
{
wenzelm@49695
    39
  require(!Platform.is_windows)
wenzelm@49695
    40
wenzelm@45027
    41
  private def mk_fifo(): String =
wenzelm@45027
    42
  {
wenzelm@45027
    43
    val i = Fifo_Channel.next_fifo()
wenzelm@45027
    44
    val script =
wenzelm@45027
    45
      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
wenzelm@45027
    46
      "echo -n \"$FIFO\"\n" +
wenzelm@45027
    47
      "mkfifo -m 600 \"$FIFO\"\n"
wenzelm@50845
    48
    val result = Isabelle_System.bash(script)
wenzelm@50845
    49
    if (result.rc == 0) result.out else error(result.err)
wenzelm@45027
    50
  }
wenzelm@45027
    51
wenzelm@49695
    52
  private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete
wenzelm@45027
    53
wenzelm@49695
    54
  private def fifo_input_stream(fifo: String): InputStream = new FileInputStream(fifo)
wenzelm@49695
    55
  private def fifo_output_stream(fifo: String): OutputStream = new FileOutputStream(fifo)
wenzelm@45027
    56
wenzelm@45027
    57
  private val fifo1 = mk_fifo()
wenzelm@45027
    58
  private val fifo2 = mk_fifo()
wenzelm@45027
    59
wenzelm@45027
    60
  val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
wenzelm@45027
    61
wenzelm@45027
    62
  def rendezvous(): (OutputStream, InputStream) =
wenzelm@45027
    63
  {
wenzelm@45027
    64
    val output_stream = fifo_output_stream(fifo1)
wenzelm@45027
    65
    val input_stream = fifo_input_stream(fifo2)
wenzelm@45027
    66
    (output_stream, input_stream)
wenzelm@45027
    67
  }
wenzelm@45027
    68
wenzelm@45027
    69
  def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
wenzelm@45027
    70
}
wenzelm@45028
    71
wenzelm@45028
    72
wenzelm@45028
    73
/** sockets **/
wenzelm@45028
    74
wenzelm@45251
    75
private class Socket_Channel extends System_Channel
wenzelm@45028
    76
{
wenzelm@45028
    77
  private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
wenzelm@45028
    78
wenzelm@45028
    79
  def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
wenzelm@45028
    80
wenzelm@45028
    81
  def rendezvous(): (OutputStream, InputStream) =
wenzelm@45028
    82
  {
wenzelm@45028
    83
    val socket = server.accept
wenzelm@45028
    84
    (socket.getOutputStream, socket.getInputStream)
wenzelm@45028
    85
  }
wenzelm@45028
    86
wenzelm@45028
    87
  def accepted() { server.close }
wenzelm@45028
    88
}