src/Pure/System/system_channel.scala
author wenzelm
Mon Oct 17 11:24:22 2011 +0200 (2011-10-17 ago)
changeset 45158 db4bf4fb5492
parent 45055 55274f7e306b
child 45243 27466646a7a3
permissions -rw-r--r--
always use sockets on Windows/Cygwin;
discontinued special raw_dump facility;
     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, FileInputStream, FileOutputStream, IOException}
    12 import java.net.{ServerSocket, InetAddress}
    13 
    14 
    15 object System_Channel
    16 {
    17   def apply(use_socket: Boolean = false): System_Channel =
    18     if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
    19 }
    20 
    21 abstract class System_Channel
    22 {
    23   def isabelle_args: List[String]
    24   def rendezvous(): (OutputStream, InputStream)
    25   def accepted(): Unit
    26 }
    27 
    28 
    29 /** named pipes **/
    30 
    31 object Fifo_Channel
    32 {
    33   private val next_fifo = new Counter
    34 }
    35 
    36 class Fifo_Channel extends System_Channel
    37 {
    38   private def mk_fifo(): String =
    39   {
    40     val i = Fifo_Channel.next_fifo()
    41     val script =
    42       "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
    43       "echo -n \"$FIFO\"\n" +
    44       "mkfifo -m 600 \"$FIFO\"\n"
    45     val (out, err, rc) = Isabelle_System.bash(script)
    46     if (rc == 0) out else error(err.trim)
    47   }
    48 
    49   private def rm_fifo(fifo: String): Boolean =
    50     Isabelle_System.platform_file(
    51       Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).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 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 }