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;
     1 /*  Title:      Pure/System/system_channel.scala
     2     Author:     Makarius
     3 
     4 Portable system channel for inter-process communication, based on
     5 named pipes or sockets.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import java.io.{InputStream, OutputStream, File => JFile, FileInputStream,
    12   FileOutputStream, IOException}
    13 import java.net.{ServerSocket, InetAddress}
    14 
    15 
    16 object System_Channel
    17 {
    18   def apply(use_socket: Boolean = false): System_Channel =
    19     if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
    20 }
    21 
    22 abstract class System_Channel
    23 {
    24   def isabelle_args: List[String]
    25   def rendezvous(): (OutputStream, InputStream)
    26   def accepted(): Unit
    27 }
    28 
    29 
    30 /** named pipes **/
    31 
    32 private object Fifo_Channel
    33 {
    34   private val next_fifo = Counter.make()
    35 }
    36 
    37 private class Fifo_Channel extends System_Channel
    38 {
    39   require(!Platform.is_windows)
    40 
    41   private def mk_fifo(): String =
    42   {
    43     val i = Fifo_Channel.next_fifo()
    44     val script =
    45       "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
    46       "echo -n \"$FIFO\"\n" +
    47       "mkfifo -m 600 \"$FIFO\"\n"
    48     val result = Isabelle_System.bash(script)
    49     if (result.rc == 0) result.out else error(result.err)
    50   }
    51 
    52   private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete
    53 
    54   private def fifo_input_stream(fifo: String): InputStream = new FileInputStream(fifo)
    55   private def fifo_output_stream(fifo: String): OutputStream = new FileOutputStream(fifo)
    56 
    57   private val fifo1 = mk_fifo()
    58   private val fifo2 = mk_fifo()
    59 
    60   val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
    61 
    62   def rendezvous(): (OutputStream, InputStream) =
    63   {
    64     val output_stream = fifo_output_stream(fifo1)
    65     val input_stream = fifo_input_stream(fifo2)
    66     (output_stream, input_stream)
    67   }
    68 
    69   def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
    70 }
    71 
    72 
    73 /** sockets **/
    74 
    75 private class Socket_Channel extends System_Channel
    76 {
    77   private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
    78 
    79   def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
    80 
    81   def rendezvous(): (OutputStream, InputStream) =
    82   {
    83     val socket = server.accept
    84     (socket.getOutputStream, socket.getInputStream)
    85   }
    86 
    87   def accepted() { server.close }
    88 }