# HG changeset patch
# User wenzelm
# Date 1316636297 -7200
# Node ID d608dd8cd409a0397706b8254354874a749c8f7e
# Parent  f459e93a038eded0022ca8ba7eb112afdb66d926
alternative Socket_Channel;
use BinIO for fifos uniformly;

diff -r f459e93a038e -r d608dd8cd409 bin/isabelle-process
--- a/bin/isabelle-process	Wed Sep 21 20:35:50 2011 +0200
+++ b/bin/isabelle-process	Wed Sep 21 22:18:17 2011 +0200
@@ -29,6 +29,7 @@
   echo "    -I           startup Isar interaction mode"
   echo "    -P           startup Proof General interaction mode"
   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 "    -X           startup PGIP interaction mode"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
@@ -61,6 +62,7 @@
 ISAR=false
 PROOFGENERAL=""
 SECURE=""
+WRAPPER_SOCKET=""
 WRAPPER_FIFOS=""
 PGIP=""
 MLTEXT=""
@@ -69,7 +71,7 @@
 READONLY=""
 NOWRITE=""
 
-while getopts "IPSW:Xe:fm:qruw" OPT
+while getopts "IPST:W:Xe:fm:qruw" OPT
 do
   case "$OPT" in
     I)
@@ -81,6 +83,9 @@
     S)
       SECURE=true
       ;;
+    T)
+      WRAPPER_SOCKET="$OPTARG"
+      ;;
     W)
       WRAPPER_FIFOS="$OPTARG"
       ;;
@@ -213,12 +218,14 @@
 
 NICE="nice"
 
-if [ -n "$WRAPPER_FIFOS" ]; then
+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[0]}\" \"${FIFOS[1]}\";"
+  MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
 elif [ -n "$PGIP" ]; then
   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
 elif [ -n "$PROOFGENERAL" ]; then
diff -r f459e93a038e -r d608dd8cd409 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Wed Sep 21 20:35:50 2011 +0200
+++ b/doc-src/System/Thy/Basics.thy	Wed Sep 21 22:18:17 2011 +0200
@@ -332,6 +332,7 @@
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
+    -T ADDR      startup process wrapper, with socket address
     -W IN:OUT    startup process wrapper, with input/output fifos
     -X           startup PGIP interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
@@ -409,11 +410,11 @@
   interaction with the Proof General user interface, and the
   @{verbatim "-X"} option enables XML-based PGIP communication.
 
-  \medskip The @{verbatim "-W"} option makes Isabelle enter a special
-  process wrapper for interaction via the Isabelle/Scala layer, 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 "-T"} or @{verbatim "-W"} option makes
+  Isabelle enter a special process wrapper for interaction via the
+  Isabelle/Scala layer, 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 "-S"} option makes the Isabelle process more
   secure by disabling some critical operations, notably runtime
diff -r f459e93a038e -r d608dd8cd409 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Wed Sep 21 20:35:50 2011 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Wed Sep 21 22:18:17 2011 +0200
@@ -343,6 +343,7 @@
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
+    -T ADDR      startup process wrapper, with socket address
     -W IN:OUT    startup process wrapper, with input/output fifos
     -X           startup PGIP interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
@@ -420,11 +421,10 @@
   interaction with the Proof General user interface, and the
   \verb|-X| option enables XML-based PGIP communication.
 
-  \medskip The \verb|-W| option makes Isabelle enter a special
-  process wrapper for interaction via the Isabelle/Scala layer, see
-  also \verb|~~/src/Pure/System/isabelle_process.scala|.  The
-  protocol between the ML and JVM process is private to the
-  implementation.
+  \medskip The \verb|-T| or \verb|-W| option makes
+  Isabelle enter a special process wrapper for interaction via the
+  Isabelle/Scala layer, see also \verb|~~/src/Pure/System/isabelle_process.scala|.  The protocol between
+  the ML and JVM process is private to the implementation.
 
   \medskip The \verb|-S| option makes the Isabelle process more
   secure by disabling some critical operations, notably runtime
diff -r f459e93a038e -r d608dd8cd409 src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Wed Sep 21 20:35:50 2011 +0200
+++ b/src/Pure/General/socket_io.ML	Wed Sep 21 22:18:17 2011 +0200
@@ -9,7 +9,7 @@
 signature SOCKET_IO =
 sig
   val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
-  val open_streams: string * int -> BinIO.instream * BinIO.outstream
+  val open_streams: string -> BinIO.instream * BinIO.outstream
 end;
 
 structure Socket_IO: SOCKET_IO =
@@ -68,15 +68,17 @@
   in (in_stream, out_stream) end;
 
 
-fun open_streams (hostname, port) =
+fun open_streams socket_name =
   let
-    val host =
-      (case NetHostDB.getByName hostname of
-        NONE => error ("Bad host name: " ^ quote hostname)
-      | SOME host => host);
-    val addr = INetSock.toAddr (NetHostDB.addr host, port);
+    fun err () = error ("Bad socket name: " ^ quote socket_name);
+    val (host, port) =
+      (case space_explode ":" socket_name of
+        [h, p] =>
+         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
+          case Int.fromString p of SOME port => port | NONE => err ())
+      | _ => err ());
     val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
-    val _ = Socket.connect (socket, addr);
+    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
   in make_streams socket end;
 
 end;
diff -r f459e93a038e -r d608dd8cd409 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Sep 21 20:35:50 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Sep 21 22:18:17 2011 +0200
@@ -21,7 +21,8 @@
   val add_command: string -> (string list -> unit) -> unit
   val command: string -> string list -> unit
   val crashes: exn list Synchronized.var
-  val init: string -> string -> unit
+  val init_socket: string -> unit
+  val init_fifos: string -> string -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
@@ -81,11 +82,11 @@
 
 fun message_output mbox out_stream =
   let
-    fun flush () = ignore (try TextIO.flushOut out_stream);
+    fun flush () = ignore (try BinIO.flushOut out_stream);
     fun loop receive =
       (case receive mbox of
         SOME (msg, do_flush) =>
-         (List.app (fn s => TextIO.output (out_stream, s)) msg;
+         (List.app (fn s => BinIO.output (out_stream, Byte.stringToBytes s)) msg;
           if do_flush then flush () else ();
           loop (Mailbox.receive_timeout (seconds 0.02)))
       | NONE => (flush (); loop (SOME o Mailbox.receive)));
@@ -93,12 +94,8 @@
 
 in
 
-fun setup_channels in_fifo out_fifo =
+fun setup_channels out_stream =
   let
-    (*rendezvous*)
-    val in_stream = TextIO.openIn in_fifo;
-    val out_stream = TextIO.openOut out_fifo;
-
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
 
@@ -114,8 +111,7 @@
     Output.Private_Hooks.raw_message_fn := message true mbox "H";
     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
     Output.Private_Hooks.prompt_fn := ignore;
-    message true mbox "A" [] (Session.welcome ());
-    in_stream
+    message true mbox "A" [] (Session.welcome ())
   end;
 
 end;
@@ -131,13 +127,25 @@
   (Synchronized.change crashes (cons crash);
     warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
 
+fun read_line stream =
+  let
+    val content = String.implode o rev;
+    fun read cs =
+      (case BinIO.input1 stream of
+        NONE => (content cs, null cs)
+      | SOME b =>
+          (case Byte.byteToChar b of
+            #"\n" => (content cs, false)
+          | c => read (c :: cs)));
+  in case read [] of ("", true) => NONE | (s, _) => SOME s end;
+
 fun read_chunk stream len =
   let
     val n =
       (case Int.fromString len of
         SOME n => n
       | NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
-    val chunk = TextIO.inputN (stream, n);
+    val chunk = Byte.bytesToString (BinIO.inputN (stream, n));
     val m = size chunk;
   in
     if m = n then chunk
@@ -145,7 +153,7 @@
   end;
 
 fun read_command stream =
-  (case TextIO.inputLine stream of
+  (case read_line stream of
     NONE => raise Runtime.TERMINATE
   | SOME line => map (read_chunk stream) (space_explode "," line));
 
@@ -170,7 +178,7 @@
 
 (* init *)
 
-fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
+fun init make_streams = ignore (Simple_Thread.fork false (fn () =>
   let
     val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
     val _ = Output.physical_stdout Symbol.STX;
@@ -186,11 +194,18 @@
         (fold (update op =)
           [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
 
-    val in_stream = setup_channels in_fifo out_fifo;
+    val (in_stream, out_stream) = make_streams ();
+    val _ = setup_channels out_stream;
+
     val _ = Keyword.status ();
     val _ = Thy_Info.status ();
     val _ = Output.status (Markup.markup Markup.ready "process ready");
   in loop in_stream end));
 
+fun rendezvous fifo1 fifo2 = (BinIO.openIn fifo1, BinIO.openOut fifo2);
+fun init_fifos fifo1 fifo2 = init (fn () => rendezvous fifo1 fifo2);
+
+fun init_socket socket_name = init (fn () => Socket_IO.open_streams socket_name);
+
 end;
 
diff -r f459e93a038e -r d608dd8cd409 src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Wed Sep 21 20:35:50 2011 +0200
+++ b/src/Pure/System/system_channel.scala	Wed Sep 21 22:18:17 2011 +0200
@@ -1,13 +1,15 @@
 /*  Title:      Pure/System/system_channel.scala
     Author:     Makarius
 
-Portable system channel for inter-process communication.
+Portable system channel for inter-process communication, based on
+named pipes or sockets.
 */
 
 package isabelle
 
 
 import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
+import java.net.{ServerSocket, InetAddress}
 
 
 object System_Channel
@@ -23,6 +25,8 @@
 }
 
 
+/** named pipes **/
+
 object Fifo_Channel
 {
   private val next_fifo = new Counter
@@ -30,8 +34,6 @@
 
 class Fifo_Channel extends System_Channel
 {
-  /* operations on named pipes */
-
   private def mk_fifo(): String =
   {
     val i = Fifo_Channel.next_fifo()
@@ -81,8 +83,6 @@
   }
 
 
-  /* initialization */
-
   private val fifo1 = mk_fifo()
   private val fifo2 = mk_fifo()
 
@@ -90,7 +90,6 @@
 
   def rendezvous(): (OutputStream, InputStream) =
   {
-    /*rendezvous*/
     val output_stream = fifo_output_stream(fifo1)
     val input_stream = fifo_input_stream(fifo2)
     (output_stream, input_stream)
@@ -98,3 +97,21 @@
 
   def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) }
 }
+
+
+/** sockets **/
+
+class Socket_Channel extends System_Channel
+{
+  private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
+
+  def isabelle_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort)
+
+  def rendezvous(): (OutputStream, InputStream) =
+  {
+    val socket = server.accept
+    (socket.getOutputStream, socket.getInputStream)
+  }
+
+  def accepted() { server.close }
+}