src/Pure/System/system_channel.scala
changeset 45028 d608dd8cd409
parent 45027 f459e93a038e
child 45055 55274f7e306b
equal deleted inserted replaced
45027:f459e93a038e 45028:d608dd8cd409
     1 /*  Title:      Pure/System/system_channel.scala
     1 /*  Title:      Pure/System/system_channel.scala
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 Portable system channel for inter-process communication.
     4 Portable system channel for inter-process communication, based on
       
     5 named pipes or sockets.
     5 */
     6 */
     6 
     7 
     7 package isabelle
     8 package isabelle
     8 
     9 
     9 
    10 
    10 import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
    11 import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
       
    12 import java.net.{ServerSocket, InetAddress}
    11 
    13 
    12 
    14 
    13 object System_Channel
    15 object System_Channel
    14 {
    16 {
    15   def apply(): System_Channel = new Fifo_Channel
    17   def apply(): System_Channel = new Fifo_Channel
    21   def rendezvous(): (OutputStream, InputStream)
    23   def rendezvous(): (OutputStream, InputStream)
    22   def accepted(): Unit
    24   def accepted(): Unit
    23 }
    25 }
    24 
    26 
    25 
    27 
       
    28 /** named pipes **/
       
    29 
    26 object Fifo_Channel
    30 object Fifo_Channel
    27 {
    31 {
    28   private val next_fifo = new Counter
    32   private val next_fifo = new Counter
    29 }
    33 }
    30 
    34 
    31 class Fifo_Channel extends System_Channel
    35 class Fifo_Channel extends System_Channel
    32 {
    36 {
    33   /* operations on named pipes */
       
    34 
       
    35   private def mk_fifo(): String =
    37   private def mk_fifo(): String =
    36   {
    38   {
    37     val i = Fifo_Channel.next_fifo()
    39     val i = Fifo_Channel.next_fifo()
    38     val script =
    40     val script =
    39       "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
    41       "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
    79     }
    81     }
    80     else new FileOutputStream(fifo)
    82     else new FileOutputStream(fifo)
    81   }
    83   }
    82 
    84 
    83 
    85 
    84   /* initialization */
       
    85 
       
    86   private val fifo1 = mk_fifo()
    86   private val fifo1 = mk_fifo()
    87   private val fifo2 = mk_fifo()
    87   private val fifo2 = mk_fifo()
    88 
    88 
    89   val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
    89   val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
    90 
    90 
    91   def rendezvous(): (OutputStream, InputStream) =
    91   def rendezvous(): (OutputStream, InputStream) =
    92   {
    92   {
    93     /*rendezvous*/
       
    94     val output_stream = fifo_output_stream(fifo1)
    93     val output_stream = fifo_output_stream(fifo1)
    95     val input_stream = fifo_input_stream(fifo2)
    94     val input_stream = fifo_input_stream(fifo2)
    96     (output_stream, input_stream)
    95     (output_stream, input_stream)
    97   }
    96   }
    98 
    97 
    99   def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
    98   def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
   100 }
    99 }
       
   100 
       
   101 
       
   102 /** sockets **/
       
   103 
       
   104 class Socket_Channel extends System_Channel
       
   105 {
       
   106   private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
       
   107 
       
   108   def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
       
   109 
       
   110   def rendezvous(): (OutputStream, InputStream) =
       
   111   {
       
   112     val socket = server.accept
       
   113     (socket.getOutputStream, socket.getInputStream)
       
   114   }
       
   115 
       
   116   def accepted() { server.close }
       
   117 }