src/Pure/System/system_channel.scala
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48409 0d2114eb412a
child 49695 8f61d1c7dded
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/system_channel.scala
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     3
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
     4
Portable system channel for inter-process communication, based on
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
     5
named pipes or sockets.
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     6
*/
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     7
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     8
package isabelle
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
     9
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    10
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
    11
import java.io.{InputStream, OutputStream, File => JFile, FileInputStream,
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
    12
  FileOutputStream, IOException}
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    13
import java.net.{ServerSocket, InetAddress}
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    14
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    15
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    16
object System_Channel
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    17
{
45055
55274f7e306b explicit option for socket vs. fifo communication;
wenzelm
parents: 45028
diff changeset
    18
  def apply(use_socket: Boolean = false): System_Channel =
45158
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45055
diff changeset
    19
    if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    20
}
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    21
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    22
abstract class System_Channel
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    23
{
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    24
  def isabelle_args: List[String]
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    25
  def rendezvous(): (OutputStream, InputStream)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    26
  def accepted(): Unit
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    27
}
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    28
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    29
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    30
/** named pipes **/
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    31
45251
12913296be79 more private stuff;
wenzelm
parents: 45243
diff changeset
    32
private object Fifo_Channel
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    33
{
45243
27466646a7a3 class Counter as abstract datatype;
wenzelm
parents: 45158
diff changeset
    34
  private val next_fifo = Counter()
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    35
}
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    36
45251
12913296be79 more private stuff;
wenzelm
parents: 45243
diff changeset
    37
private class Fifo_Channel extends System_Channel
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    38
{
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    39
  private def mk_fifo(): String =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    40
  {
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    41
    val i = Fifo_Channel.next_fifo()
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    42
    val script =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    43
      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    44
      "echo -n \"$FIFO\"\n" +
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    45
      "mkfifo -m 600 \"$FIFO\"\n"
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    46
    val (out, err, rc) = Isabelle_System.bash(script)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    47
    if (rc == 0) out else error(err.trim)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    48
  }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    49
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    50
  private def rm_fifo(fifo: String): Boolean =
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 45251
diff changeset
    51
    Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo).file.delete
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    52
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    53
  private def fifo_input_stream(fifo: String): InputStream =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    54
  {
45158
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45055
diff changeset
    55
    require(!Platform.is_windows)
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45055
diff changeset
    56
    new FileInputStream(fifo)
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    57
  }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    58
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    59
  private def fifo_output_stream(fifo: String): OutputStream =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    60
  {
45158
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45055
diff changeset
    61
    require(!Platform.is_windows)
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45055
diff changeset
    62
    new FileOutputStream(fifo)
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    63
  }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    64
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    65
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    66
  private val fifo1 = mk_fifo()
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    67
  private val fifo2 = mk_fifo()
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    68
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    69
  val isabelle_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    70
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    71
  def rendezvous(): (OutputStream, InputStream) =
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    72
  {
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    73
    val output_stream = fifo_output_stream(fifo1)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    74
    val input_stream = fifo_input_stream(fifo2)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    75
    (output_stream, input_stream)
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    76
  }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    77
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    78
  def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
diff changeset
    79
}
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    80
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    81
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    82
/** sockets **/
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    83
45251
12913296be79 more private stuff;
wenzelm
parents: 45243
diff changeset
    84
private class Socket_Channel extends System_Channel
45028
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    85
{
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    86
  private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    87
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    88
  def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    89
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    90
  def rendezvous(): (OutputStream, InputStream) =
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    91
  {
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    92
    val socket = server.accept
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    93
    (socket.getOutputStream, socket.getInputStream)
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    94
  }
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    95
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    96
  def accepted() { server.close }
d608dd8cd409 alternative Socket_Channel;
wenzelm
parents: 45027
diff changeset
    97
}