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};
     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()
    35 }
    36 
    37 private class Fifo_Channel extends System_Channel
    38 {
    39   private def mk_fifo(): String =
    40   {
    41     val i = Fifo_Channel.next_fifo()
    42     val script =
    43       "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
    44       "echo -n \"$FIFO\"\n" +
    45       "mkfifo -m 600 \"$FIFO\"\n"
    46     val (out, err, rc) = Isabelle_System.bash(script)
    47     if (rc == 0) out else error(err.trim)
    48   }
    49 
    50   private def rm_fifo(fifo: String): Boolean =
    51     Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo).file.delete
    52 
    53   private def fifo_input_stream(fifo: String): InputStream =
    54   {
    55     require(!Platform.is_windows)
    56     new FileInputStream(fifo)
    57   }
    58 
    59   private def fifo_output_stream(fifo: String): OutputStream =
    60   {
    61     require(!Platform.is_windows)
    62     new FileOutputStream(fifo)
    63   }
    64 
    65 
    66   private val fifo1 = mk_fifo()
    67   private val fifo2 = mk_fifo()
    68 
    69   val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
    70 
    71   def rendezvous(): (OutputStream, InputStream) =
    72   {
    73     val output_stream = fifo_output_stream(fifo1)
    74     val input_stream = fifo_input_stream(fifo2)
    75     (output_stream, input_stream)
    76   }
    77 
    78   def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
    79 }
    80 
    81 
    82 /** sockets **/
    83 
    84 private class Socket_Channel extends System_Channel
    85 {
    86   private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
    87 
    88   def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
    89 
    90   def rendezvous(): (OutputStream, InputStream) =
    91   {
    92     val socket = server.accept
    93     (socket.getOutputStream, socket.getInputStream)
    94   }
    95 
    96   def accepted() { server.close }
    97 }