# HG changeset patch
# User wenzelm
# Date 1421005214 -3600
# Node ID acba5d6fdb2f6941699e8c17e34ff4f4a45dc043
# Parent  3bde948f439cdc5d4181f3cfdc5d33005c8a3705
discontinued fifo channel, always use portable socket;

diff -r 3bde948f439c -r acba5d6fdb2f bin/isabelle_process
--- a/bin/isabelle_process	Sun Jan 11 13:44:25 2015 +0100
+++ b/bin/isabelle_process	Sun Jan 11 20:40:14 2015 +0100
@@ -27,9 +27,8 @@
   echo
   echo "  Options are:"
   echo "    -O           system options from given YXML file"
+  echo "    -P SOCKET    startup process wrapper via TCP socket"
   echo "    -S           secure mode -- disallow critical operations"
-  echo "    -T ADDR      startup process wrapper, with socket address"
-  echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -m MODE      add print mode for output"
   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
@@ -57,9 +56,8 @@
 # options
 
 OPTIONS_FILE=""
+PROCESS_SOCKET=""
 SECURE=""
-WRAPPER_SOCKET=""
-WRAPPER_FIFOS=""
 MLTEXT=""
 MODES=""
 declare -a SYSTEM_OPTIONS=()
@@ -67,21 +65,18 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "O:ST:W:e:m:o:qrw" OPT
+while getopts "O:P:Se:m:o:qrw" OPT
 do
   case "$OPT" in
     O)
       OPTIONS_FILE="$OPTARG"
       ;;
+    P)
+      PROCESS_SOCKET="$OPTARG"
+      ;;
     S)
       SECURE=true
       ;;
-    T)
-      WRAPPER_SOCKET="$OPTARG"
-      ;;
-    W)
-      WRAPPER_FIFOS="$OPTARG"
-      ;;
     e)
       MLTEXT="$MLTEXT $OPTARG"
       ;;
@@ -203,14 +198,8 @@
 
 [ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
 
-if [ -n "$WRAPPER_SOCKET" ]; then
-  MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
-elif [ -n "$WRAPPER_FIFOS" ]; then
-  splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
-  [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
-  [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
-  [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
-  MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
+if [ -n "$PROCESS_SOCKET" ]; then
+  MLTEXT="$MLTEXT; Isabelle_Process.init \"$PROCESS_SOCKET\";"
 else
   ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
   if [ -n "$OPTIONS_FILE" ]; then
diff -r 3bde948f439c -r acba5d6fdb2f src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Sun Jan 11 13:44:25 2015 +0100
+++ b/src/Doc/System/Basics.thy	Sun Jan 11 20:40:14 2015 +0100
@@ -362,9 +362,8 @@
 
   Options are:
     -O           system options from given YXML file
+    -P SOCKET    startup process wrapper via TCP socket
     -S           secure mode -- disallow critical operations
-    -T ADDR      startup process wrapper, with socket address
-    -W IN:OUT    startup process wrapper, with input/output fifos
     -e MLTEXT    pass MLTEXT to the ML session
     -m MODE      add print mode for output
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
@@ -433,11 +432,11 @@
   system options as a file in YXML format (according to the Isabelle/Scala
   function @{verbatim isabelle.Options.encode}).
 
-  \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
-  Isabelle enter a special process wrapper for interaction via
-  Isabelle/Scala, see also @{file
-  "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
-  the ML and JVM process is private to the implementation.
+  \medskip The @{verbatim "-P"} option starts the Isabelle process wrapper
+  for Isabelle/Scala, with a private protocol running over the specified TCP
+  socket. Isabelle/ML and Isabelle/Scala provide various programming
+  interfaces to invoke protocol functions over untyped strings and XML
+  trees.
 
   \medskip The @{verbatim "-S"} option makes the Isabelle process more
   secure by disabling some critical operations, notably runtime
diff -r 3bde948f439c -r acba5d6fdb2f src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sun Jan 11 13:44:25 2015 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sun Jan 11 20:40:14 2015 +0100
@@ -10,8 +10,7 @@
   val protocol_command: string -> (string list -> unit) -> unit
   val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
-  val init_fifos: string -> string -> unit
-  val init_socket: string -> unit
+  val init: string -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
@@ -189,7 +188,7 @@
 val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
 val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
 
-val init = uninterruptible (fn _ => fn rendezvous =>
+val init = uninterruptible (fn _ => fn socket =>
   let
     val _ = SHA1_Samples.test ()
       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn);
@@ -201,14 +200,11 @@
       Unsynchronized.change print_mode
         (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
 
-    val channel = rendezvous ();
+    val channel = System_Channel.rendezvous socket;
     val msg_channel = init_channels channel;
     val _ = Session.init_protocol_handlers ();
     val _ = loop channel;
   in Message_Channel.shutdown msg_channel end);
 
-fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
-fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
-
 end;
 
diff -r 3bde948f439c -r acba5d6fdb2f src/Pure/System/system_channel.ML
--- a/src/Pure/System/system_channel.ML	Sun Jan 11 13:44:25 2015 +0100
+++ b/src/Pure/System/system_channel.ML	Sun Jan 11 20:40:14 2015 +0100
@@ -1,8 +1,7 @@
 (*  Title:      Pure/System/system_channel.ML
     Author:     Makarius
 
-Portable system channel for inter-process communication, based on
-named pipes or sockets.
+Socket-based system channel for inter-process communication.
 *)
 
 signature SYSTEM_CHANNEL =
@@ -12,44 +11,15 @@
   val inputN: T -> int -> string
   val output: T -> string -> unit
   val flush: T -> unit
-  val fifo_rendezvous: string -> string -> T
-  val socket_rendezvous: string -> T
+  val rendezvous: string -> T
 end;
 
 structure System_Channel: SYSTEM_CHANNEL =
 struct
 
-datatype T = System_Channel of
- {input_line: unit -> string option,
-  inputN: int -> string,
-  output: string -> unit,
-  flush: unit -> unit};
-
-fun input_line (System_Channel {input_line = f, ...}) = f ();
-fun inputN (System_Channel {inputN = f, ...}) n = f n;
-fun output (System_Channel {output = f, ...}) s = f s;
-fun flush (System_Channel {flush = f, ...}) = f ();
-
-
-(* named pipes *)
+datatype T = System_Channel of BinIO.instream * BinIO.outstream;
 
-fun fifo_rendezvous fifo1 fifo2 =
-  let
-    val in_stream = TextIO.openIn fifo1;
-    val out_stream = TextIO.openOut fifo2;
-    val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream out_stream, IO.BLOCK_BUF);
-  in
-    System_Channel
-     {input_line = fn () => TextIO.inputLine in_stream,
-      inputN = fn n => TextIO.inputN (in_stream, n),
-      output = fn s => TextIO.output (out_stream, s),
-      flush = fn () => TextIO.flushOut out_stream}
-  end;
-
-
-(* sockets *)
-
-fun read_line in_stream =
+fun input_line (System_Channel (in_stream, _)) =
   let
     fun result cs = String.implode (rev (#"\n" :: cs));
     fun read cs =
@@ -61,19 +31,21 @@
           | c => read (c :: cs)));
   in read [] end;
 
-fun socket_rendezvous name =
+fun inputN (System_Channel (in_stream, _)) n =
+  if n = 0 then ""  (*workaround for polyml-5.5.1 or earlier*)
+  else Byte.bytesToString (BinIO.inputN (in_stream, n));
+
+fun output (System_Channel (_, out_stream)) s =
+  BinIO.output (out_stream, Byte.stringToBytes s);
+
+fun flush (System_Channel (_, out_stream)) =
+  BinIO.flushOut out_stream;
+
+fun rendezvous name =
   let
     val (in_stream, out_stream) = Socket_IO.open_streams name;
     val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
-  in
-    System_Channel
-     {input_line = fn () => read_line in_stream,
-      inputN = fn n =>
-        if n = 0 then ""  (*workaround for polyml-5.5.1 or earlier*)
-        else Byte.bytesToString (BinIO.inputN (in_stream, n)),
-      output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
-      flush = fn () => BinIO.flushOut out_stream}
-  end;
+  in System_Channel (in_stream, out_stream) end;
 
 end;
 
diff -r 3bde948f439c -r acba5d6fdb2f src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Sun Jan 11 13:44:25 2015 +0100
+++ b/src/Pure/System/system_channel.scala	Sun Jan 11 20:40:14 2015 +0100
@@ -1,87 +1,28 @@
 /*  Title:      Pure/System/system_channel.scala
     Author:     Makarius
 
-Portable system channel for inter-process communication, based on
-named pipes or sockets.
+Socket-based system channel for inter-process communication.
 */
 
 package isabelle
 
 
-import java.io.{InputStream, OutputStream, File => JFile, FileInputStream,
-  FileOutputStream, IOException}
+import java.io.{InputStream, OutputStream}
 import java.net.{ServerSocket, InetAddress}
 
 
 object System_Channel
 {
-  def apply(): System_Channel = new Socket_Channel
-    // FIXME if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
-}
-
-abstract class System_Channel
-{
-  def params: List[String]
-  def prover_args: List[String]
-  def rendezvous(): (OutputStream, InputStream)
-  def accepted(): Unit
-}
-
-
-/** named pipes **/
-
-private object Fifo_Channel
-{
-  private val next_fifo = Counter.make()
+  def apply(): System_Channel = new System_Channel
 }
 
-private class Fifo_Channel extends System_Channel
-{
-  require(!Platform.is_windows)
-
-  private def mk_fifo(): String =
-  {
-    val i = Fifo_Channel.next_fifo()
-    val script =
-      "FIFO=\"${TMPDIR:-/tmp}/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
-      "echo -n \"$FIFO\"\n" +
-      "mkfifo -m 600 \"$FIFO\"\n"
-    val result = Isabelle_System.bash(script)
-    if (result.rc == 0) result.out else error(result.err)
-  }
-
-  private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete
-
-  private def fifo_input_stream(fifo: String): InputStream = new FileInputStream(fifo)
-  private def fifo_output_stream(fifo: String): OutputStream = new FileOutputStream(fifo)
-
-  private val fifo1 = mk_fifo()
-  private val fifo2 = mk_fifo()
-
-  def params: List[String] = List(fifo1, fifo2)
-
-  val prover_args: List[String] = List ("-W", fifo1 + ":" + fifo2)
-
-  def rendezvous(): (OutputStream, InputStream) =
-  {
-    val output_stream = fifo_output_stream(fifo1)
-    val input_stream = fifo_input_stream(fifo2)
-    (output_stream, input_stream)
-  }
-
-  def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
-}
-
-
-/** sockets **/
-
-private class Socket_Channel extends System_Channel
+class System_Channel private
 {
   private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
 
   def params: List[String] = List("127.0.0.1", server.getLocalPort.toString)
 
-  def prover_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
+  def prover_args: List[String] = List("-P", "127.0.0.1:" + server.getLocalPort)
 
   def rendezvous(): (OutputStream, InputStream) =
   {