# HG changeset patch
# User wenzelm
# Date 1316729489 -7200
# Node ID d51bc5756650eb99310d907f1e0022767ebe3b3e
# Parent  c478d187637140d40aeaeef38be8b063f2043952# Parent  9cf265a192f68fc5d3ddf3e7a9d21678597b79d6
merged;

diff -r c478d1876371 -r d51bc5756650 bin/isabelle-process
--- a/bin/isabelle-process	Thu Sep 22 14:12:16 2011 -0700
+++ b/bin/isabelle-process	Fri Sep 23 00:11:29 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 c478d1876371 -r d51bc5756650 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Thu Sep 22 14:12:16 2011 -0700
+++ b/doc-src/System/Thy/Basics.thy	Fri Sep 23 00:11:29 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 c478d1876371 -r d51bc5756650 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Thu Sep 22 14:12:16 2011 -0700
+++ b/doc-src/System/Thy/document/Basics.tex	Fri Sep 23 00:11:29 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 c478d1876371 -r d51bc5756650 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Sep 23 00:11:29 2011 +0200
@@ -125,9 +125,10 @@
       error ("The SMT solver Z3 may only be used for non-commercial " ^
         "applications.")
   | Z3_Non_Commercial_Unknown =>
-      error ("The SMT solver Z3 is not activated. To activate it, set " ^
-        "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^
-        "."))
+      error ("The SMT solver Z3 is not activated. To activate it, set\n" ^
+        "the environment variable " ^ quote flagN ^ " to " ^ quote "yes" ^ "." ^
+        (if getenv "Z3_COMPONENT" = "" then ""
+         else "\nSee also " ^ Path.print (Path.expand (Path.explode "$Z3_COMPONENT/etc/settings")))))
 
 end
 
diff -r c478d1876371 -r d51bc5756650 src/Pure/General/socket_io.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/socket_io.ML	Fri Sep 23 00:11:29 2011 +0200
@@ -0,0 +1,85 @@
+(*  Title:      Pure/General/socket_io.ML
+    Author:     Timothy Bourke, NICTA
+    Author:     Makarius
+
+Stream IO over TCP sockets.  Following example 10.2 in "The Standard
+ML Basis Library" by Emden R. Gansner and John H. Reppy.
+*)
+
+signature SOCKET_IO =
+sig
+  val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
+  val open_streams: string -> BinIO.instream * BinIO.outstream
+end;
+
+structure Socket_IO: SOCKET_IO =
+struct
+
+fun make_streams socket =
+  let
+    val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
+    val name = NetHostDB.toString host ^ ":" ^ string_of_int port;
+
+    val rd =
+      BinPrimIO.RD {
+        name = name,
+        chunkSize = Socket.Ctl.getRCVBUF socket,
+        readVec = SOME (fn n => Socket.recvVec (socket, n)),
+        readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
+        readVecNB = NONE,
+        readArrNB = NONE,
+        block = NONE,
+        canInput = NONE,
+        avail = fn () => NONE,
+        getPos = NONE,
+        setPos = NONE,
+        endPos = NONE,
+        verifyPos = NONE,
+        close = fn () => Socket.close socket,
+        ioDesc = NONE
+      };
+
+    val wr =
+      BinPrimIO.WR {
+        name = name,
+        chunkSize = Socket.Ctl.getSNDBUF socket,
+        writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
+        writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
+        writeVecNB = NONE,
+        writeArrNB = NONE,
+        block = NONE,
+        canOutput = NONE,
+        getPos = NONE,
+        setPos = NONE,
+        endPos = NONE,
+        verifyPos = NONE,
+        close = fn () => Socket.close socket,
+        ioDesc = NONE
+      };
+
+    val in_stream =
+      BinIO.mkInstream
+        (BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
+
+    val out_stream =
+      BinIO.mkOutstream
+        (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
+
+  in (in_stream, out_stream) end;
+
+
+fun open_streams socket_name =
+  let
+    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, INetSock.toAddr (NetHostDB.addr host, port));
+  in make_streams socket end;
+
+end;
+
diff -r c478d1876371 -r d51bc5756650 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Pure/IsaMakefile	Fri Sep 23 00:11:29 2011 +0200
@@ -98,6 +98,7 @@
   General/seq.ML					\
   General/sha1.ML					\
   General/sha1_polyml.ML				\
+  General/socket_io.ML					\
   General/source.ML					\
   General/stack.ML					\
   General/symbol.ML					\
@@ -194,6 +195,7 @@
   System/isabelle_system.ML				\
   System/isar.ML					\
   System/session.ML					\
+  System/system_channel.ML				\
   Thy/html.ML						\
   Thy/latex.ML						\
   Thy/present.ML					\
diff -r c478d1876371 -r d51bc5756650 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Pure/ML-Systems/proper_int.ML	Fri Sep 23 00:11:29 2011 +0200
@@ -226,6 +226,16 @@
 end;
 
 
+(* BinIO *)
+
+structure BinIO =
+struct
+  open BinIO;
+  fun inputN (a, b) = BinIO.inputN (a, dest_int b);
+  fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
+end;
+
+
 (* Time *)
 
 structure Time =
@@ -234,3 +244,13 @@
   fun fmt a b = Time.fmt (dest_int a) b;
 end;
 
+
+(* Sockets *)
+
+structure INetSock =
+struct
+  open INetSock;
+  fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
+  fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
+end;
+
diff -r c478d1876371 -r d51bc5756650 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Pure/ROOT.ML	Fri Sep 23 00:11:29 2011 +0200
@@ -57,6 +57,7 @@
 use "General/path.ML";
 use "General/url.ML";
 use "General/file.ML";
+use "General/socket_io.ML";
 use "General/long_name.ML";
 use "General/binding.ML";
 
@@ -266,6 +267,7 @@
 (* Isabelle/Isar system *)
 
 use "System/session.ML";
+use "System/system_channel.ML";
 use "System/isabelle_process.ML";
 use "System/invoke_scala.ML";
 use "PIDE/isar_document.ML";
diff -r c478d1876371 -r d51bc5756650 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Pure/System/isabelle_process.ML	Fri Sep 23 00:11:29 2011 +0200
@@ -9,7 +9,7 @@
   . stdout \002: ML running
   .. stdin/stdout/stderr freely available (raw ML loop)
   .. protocol thread initialization
-  ... switch to in_fifo/out_fifo channels (rendezvous via open)
+  ... rendezvous on system channel
   ... out_fifo INIT(pid): channels ready
   ... out_fifo STATUS(keywords)
   ... out_fifo READY: main loop ready
@@ -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_fifos: string -> string -> unit
+  val init_socket: string -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
@@ -79,13 +80,13 @@
       ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
         (Position.properties_of (Position.thread_data ()))) body;
 
-fun message_output mbox out_stream =
+fun message_output mbox channel =
   let
-    fun flush () = ignore (try TextIO.flushOut out_stream);
+    fun flush () = ignore (try System_Channel.flush channel);
     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 => System_Channel.output channel s) msg;
           if do_flush then flush () else ();
           loop (Mailbox.receive_timeout (seconds 0.02)))
       | NONE => (flush (); loop (SOME o Mailbox.receive)));
@@ -93,17 +94,13 @@
 
 in
 
-fun setup_channels in_fifo out_fifo =
+fun setup_channels channel =
   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);
 
     val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
-    val _ = Simple_Thread.fork false (message_output mbox out_stream);
+    val _ = Simple_Thread.fork false (message_output mbox channel);
   in
     Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
     Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
@@ -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,23 +127,23 @@
   (Synchronized.change crashes (cons crash);
     warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
 
-fun read_chunk stream len =
+fun read_chunk channel 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 = System_Channel.inputN channel n;
     val m = size chunk;
   in
     if m = n then chunk
     else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")")
   end;
 
-fun read_command stream =
-  (case TextIO.inputLine stream of
+fun read_command channel =
+  (case System_Channel.input_line channel of
     NONE => raise Runtime.TERMINATE
-  | SOME line => map (read_chunk stream) (space_explode "," line));
+  | SOME line => map (read_chunk channel) (space_explode "," line));
 
 fun run_command name args =
   Runtime.debugging (command name) args
@@ -156,21 +152,21 @@
 
 in
 
-fun loop stream =
+fun loop channel =
   let val continue =
-    (case read_command stream of
+    (case read_command channel of
       [] => (Output.error_msg "Isabelle process: no input"; true)
     | name :: args => (run_command name args; true))
     handle Runtime.TERMINATE => false
       | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
-  in if continue then loop stream else () end;
+  in if continue then loop channel else () end;
 
 end;
 
 
 (* init *)
 
-fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
+fun init rendezvous = 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 +182,16 @@
         (fold (update op =)
           [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
 
-    val in_stream = setup_channels in_fifo out_fifo;
+    val channel = rendezvous ();
+    val _ = setup_channels channel;
+
     val _ = Keyword.status ();
     val _ = Thy_Info.status ();
     val _ = Output.status (Markup.markup Markup.ready "process ready");
-  in loop in_stream end));
+  in loop 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 c478d1876371 -r d51bc5756650 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Pure/System/isabelle_process.scala	Fri Sep 23 00:11:29 2011 +0200
@@ -96,7 +96,7 @@
 
   private def put_result(kind: String, props: Properties.T, body: XML.Body)
   {
-    if (kind == Markup.INIT) rm_fifos()
+    if (kind == Markup.INIT) system_channel.accepted()
     if (kind == Markup.RAW)
       receiver(new Result(XML.Elem(Markup(kind, props), body)))
     else {
@@ -131,18 +131,16 @@
 
   /** process manager **/
 
-  private val in_fifo = Isabelle_System.mk_fifo()
-  private val out_fifo = Isabelle_System.mk_fifo()
-  private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) }
+  private val system_channel = System_Channel()
 
   private val process =
     try {
       val cmdline =
-        List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W",
-          in_fifo + ":" + out_fifo) ++ args
+        Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
+          (system_channel.isabelle_args ::: args.toList)
       new Isabelle_System.Managed_Process(true, cmdline: _*)
     }
-    catch { case e: IOException => rm_fifos(); throw(e) }
+    catch { case e: IOException => system_channel.accepted(); throw(e) }
 
   val process_result =
     Simple_Thread.future("process_result") { process.join }
@@ -182,9 +180,7 @@
       process_result.join
     }
     else {
-      // rendezvous
-      val command_stream = Isabelle_System.fifo_output_stream(in_fifo)
-      val message_stream = Isabelle_System.fifo_input_stream(out_fifo)
+      val (command_stream, message_stream) = system_channel.rendezvous()
 
       standard_input = stdin_actor()
       val stdout = stdout_actor()
@@ -197,7 +193,7 @@
       system_result("process_manager terminated")
       put_result(Markup.EXIT, "Return code: " + rc.toString)
     }
-    rm_fifos()
+    system_channel.accepted()
   }
 
 
diff -r c478d1876371 -r d51bc5756650 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Pure/System/isabelle_system.scala	Fri Sep 23 00:11:29 2011 +0200
@@ -10,8 +10,8 @@
 import java.lang.System
 import java.util.regex.Pattern
 import java.util.Locale
-import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
-  BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter, IOException}
+import java.io.{InputStream, OutputStream, File, BufferedReader, InputStreamReader,
+  BufferedWriter, OutputStreamWriter, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 import java.awt.font.TextAttribute
 
@@ -108,7 +108,7 @@
   def standard_path(path: Path): String = path.expand.implode
 
   def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
-  def platform_file(path: Path) = new File(platform_path(path))
+  def platform_file(path: Path): File = new File(platform_path(path))
 
   def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
 
@@ -266,54 +266,6 @@
   }
 
 
-  /* named pipes */
-
-  private val next_fifo = new Counter
-
-  def mk_fifo(): String =
-  {
-    val i = next_fifo()
-    val script =
-      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
-      "echo -n \"$FIFO\"\n" +
-      "mkfifo -m 600 \"$FIFO\"\n"
-    val (out, err, rc) = bash(script)
-    if (rc == 0) out else error(err.trim)
-  }
-
-  def rm_fifo(fifo: String): Boolean =
-    (new File(standard_system.jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
-
-  def fifo_input_stream(fifo: String): InputStream =
-  {
-    if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
-      val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
-      proc.getOutputStream.close
-      proc.getErrorStream.close
-      proc.getInputStream
-    }
-    else new FileInputStream(fifo)
-  }
-
-  def fifo_output_stream(fifo: String): OutputStream =
-  {
-    if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
-      val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
-      proc.getInputStream.close
-      proc.getErrorStream.close
-      val out = proc.getOutputStream
-      new OutputStream {
-        override def close() { out.close(); proc.waitFor() }
-        override def flush() { out.flush() }
-        override def write(b: Array[Byte]) { out.write(b) }
-        override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
-        override def write(b: Int) { out.write(b) }
-      }
-    }
-    else new FileOutputStream(fifo)
-  }
-
-
 
   /** Isabelle resources **/
 
diff -r c478d1876371 -r d51bc5756650 src/Pure/System/system_channel.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/system_channel.ML	Fri Sep 23 00:11:29 2011 +0200
@@ -0,0 +1,77 @@
+(*  Title:      Pure/System/system_channel.ML
+    Author:     Makarius
+
+Portable system channel for inter-process communication, based on
+named pipes or sockets.
+*)
+
+signature SYSTEM_CHANNEL =
+sig
+  type T
+  val input_line: T -> string option
+  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
+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 *)
+
+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 =
+  let
+    fun result cs = String.implode (rev (#"\n" :: cs));
+    fun read cs =
+      (case BinIO.input1 in_stream of
+        NONE => if null cs then NONE else SOME (result cs)
+      | SOME b =>
+          (case Byte.byteToChar b of
+            #"\n" => SOME (result cs)
+          | c => read (c :: cs)));
+  in read [] end;
+
+fun socket_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 => Byte.bytesToString (BinIO.inputN (in_stream, n)),
+      output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
+      flush = fn () => BinIO.flushOut out_stream}
+  end;
+
+end;
+
diff -r c478d1876371 -r d51bc5756650 src/Pure/System/system_channel.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/system_channel.scala	Fri Sep 23 00:11:29 2011 +0200
@@ -0,0 +1,117 @@
+/*  Title:      Pure/System/system_channel.scala
+    Author:     Makarius
+
+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
+{
+  def apply(): System_Channel = new Fifo_Channel
+}
+
+abstract class System_Channel
+{
+  def isabelle_args: List[String]
+  def rendezvous(): (OutputStream, InputStream)
+  def accepted(): Unit
+}
+
+
+/** named pipes **/
+
+object Fifo_Channel
+{
+  private val next_fifo = new Counter
+}
+
+class Fifo_Channel extends System_Channel
+{
+  private def mk_fifo(): String =
+  {
+    val i = Fifo_Channel.next_fifo()
+    val script =
+      "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
+      "echo -n \"$FIFO\"\n" +
+      "mkfifo -m 600 \"$FIFO\"\n"
+    val (out, err, rc) = Isabelle_System.bash(script)
+    if (rc == 0) out else error(err.trim)
+  }
+
+  private def rm_fifo(fifo: String): Boolean =
+    Isabelle_System.platform_file(
+      Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).delete
+
+  private def fifo_input_stream(fifo: String): InputStream =
+  {
+    if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
+      val proc =
+        Isabelle_System.execute(false,
+          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
+      proc.getOutputStream.close
+      proc.getErrorStream.close
+      proc.getInputStream
+    }
+    else new FileInputStream(fifo)
+  }
+
+  private def fifo_output_stream(fifo: String): OutputStream =
+  {
+    if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
+      val proc =
+        Isabelle_System.execute(false,
+          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
+      proc.getInputStream.close
+      proc.getErrorStream.close
+      val out = proc.getOutputStream
+      new OutputStream {
+        override def close() { out.close(); proc.waitFor() }
+        override def flush() { out.flush() }
+        override def write(b: Array[Byte]) { out.write(b) }
+        override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
+        override def write(b: Int) { out.write(b) }
+      }
+    }
+    else new FileOutputStream(fifo)
+  }
+
+
+  private val fifo1 = mk_fifo()
+  private val fifo2 = mk_fifo()
+
+  val isabelle_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 **/
+
+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 }
+}
diff -r c478d1876371 -r d51bc5756650 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Pure/build-jars	Fri Sep 23 00:11:29 2011 +0200
@@ -49,6 +49,7 @@
   System/session_manager.scala
   System/standard_system.scala
   System/swing_thread.scala
+  System/system_channel.scala
   Thy/completion.scala
   Thy/html.scala
   Thy/thy_header.scala
diff -r c478d1876371 -r d51bc5756650 src/Tools/WWW_Find/IsaMakefile
--- a/src/Tools/WWW_Find/IsaMakefile	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Tools/WWW_Find/IsaMakefile	Fri Sep 23 00:11:29 2011 +0200
@@ -28,10 +28,10 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
 
-$(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML \
-  html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML \
-  scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML yxml_find_theorems.ML \
-  ROOT.ML
+$(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML	\
+  html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML	\
+  scgi_server.ML server_socket.ML unicode_symbols.ML xhtml.ML		\
+  yxml_find_theorems.ML ROOT.ML
 	@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
 
 
diff -r c478d1876371 -r d51bc5756650 src/Tools/WWW_Find/ROOT.ML
--- a/src/Tools/WWW_Find/ROOT.ML	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Tools/WWW_Find/ROOT.ML	Fri Sep 23 00:11:29 2011 +0200
@@ -5,7 +5,7 @@
   use "http_status.ML";
   use "http_util.ML";
   use "xhtml.ML";
-  use "socket_util.ML";
+  use "server_socket.ML";
   use "scgi_req.ML";
   use "scgi_server.ML";
   use "echo.ML";
diff -r c478d1876371 -r d51bc5756650 src/Tools/WWW_Find/scgi_server.ML
--- a/src/Tools/WWW_Find/scgi_server.ML	Thu Sep 22 14:12:16 2011 -0700
+++ b/src/Tools/WWW_Find/scgi_server.ML	Fri Sep 23 00:11:29 2011 +0200
@@ -35,7 +35,7 @@
 
 fun server server_prefix port =
   let
-    val passive_sock = SocketUtil.init_server_socket (SOME "localhost") port;
+    val passive_sock = Server_Socket.init (SOME "localhost") port;
 
     val thread_wait = ConditionVar.conditionVar ();
     val thread_wait_mutex = Mutex.mutex ();
@@ -63,7 +63,7 @@
       let
         val (sock, _)= Socket.accept passive_sock;
 
-        val (sin, sout) = SocketUtil.make_streams sock;
+        val (sin, sout) = Socket_IO.make_streams sock;
 
         fun send msg = BinIO.output (sout, Byte.stringToBytes msg);
         fun send_log msg = (tracing msg; send msg);
diff -r c478d1876371 -r d51bc5756650 src/Tools/WWW_Find/server_socket.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/server_socket.ML	Fri Sep 23 00:11:29 2011 +0200
@@ -0,0 +1,33 @@
+(*  Title:      Tools/WWW_Find/socket_util.ML
+    Author:     Timothy Bourke, NICTA
+
+Server sockets.
+*)
+
+signature SERVER_SOCKET =
+sig
+  val init: string option -> int -> Socket.passive INetSock.stream_sock
+end;
+
+structure Server_Socket: SERVER_SOCKET =
+struct
+
+fun init opt_host port =
+  let
+    val sock = INetSock.TCP.socket ();
+    val addr =
+      (case opt_host of
+         NONE => INetSock.any port
+       | SOME host =>
+           NetHostDB.getByName host
+           |> the
+           |> NetHostDB.addr
+           |> rpair port
+           |> INetSock.toAddr
+           handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
+    val _ = Socket.bind (sock, addr);
+    val _ = Socket.listen (sock, 5);
+  in sock end;
+
+end;
+
diff -r c478d1876371 -r d51bc5756650 src/Tools/WWW_Find/socket_util.ML
--- a/src/Tools/WWW_Find/socket_util.ML	Thu Sep 22 14:12:16 2011 -0700
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(*  Title:      Tools/WWW_Find/socket_util.ML
-    Author:     Emden R. Gansner and John H. Reppy
-                SML Basis Library, section 10
-
-Routines for working with sockets.
-*)
-
-signature SOCKET_UTIL =
-sig
-  val init_server_socket : string option -> int ->
-                           Socket.passive INetSock.stream_sock
-
-  val make_streams : Socket.active INetSock.stream_sock
-                     -> BinIO.instream * BinIO.outstream
-end;
-
-structure SocketUtil =
-struct
-
-fun init_server_socket hosto port =
-  let
-    val sock = INetSock.TCP.socket ();
-    val addr =
-      (case hosto of
-         NONE => INetSock.any port
-       | SOME host =>
-           NetHostDB.getByName host
-           |> the
-           |> NetHostDB.addr
-           |> rpair port
-           |> INetSock.toAddr
-           handle Option => raise Fail ("Cannot resolve hostname: " ^ host));
-  in
-    Socket.bind (sock, addr);
-    Socket.listen (sock, 5);
-    sock
-  end;
-
-fun make_streams sock =
-  let
-    val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
-
-    val sock_name =
-      implode [ NetHostDB.toString haddr, ":", string_of_int port ];
-
-    val rd =
-      BinPrimIO.RD {
-        name = sock_name,
-        chunkSize = Socket.Ctl.getRCVBUF sock,
-        readVec = SOME (fn sz => Socket.recvVec (sock, sz)),
-        readArr = SOME (fn buffer => Socket.recvArr (sock, buffer)),
-        readVecNB = NONE,
-        readArrNB = NONE,
-        block = NONE,
-        canInput = NONE,
-        avail = fn () => NONE,
-        getPos = NONE,
-        setPos = NONE,
-        endPos = NONE,
-        verifyPos = NONE,
-        close = fn () => Socket.close sock,
-        ioDesc = NONE
-      };
-
-    val wr =
-      BinPrimIO.WR {
-        name = sock_name,
-        chunkSize = Socket.Ctl.getSNDBUF sock,
-        writeVec = SOME (fn buffer => Socket.sendVec (sock, buffer)),
-        writeArr = SOME (fn buffer => Socket.sendArr (sock, buffer)),
-        writeVecNB = NONE,
-        writeArrNB = NONE,
-        block = NONE,
-        canOutput = NONE,
-        getPos = NONE,
-        setPos = NONE,
-        endPos = NONE,
-        verifyPos = NONE,
-        close = fn () => Socket.close sock,
-        ioDesc = NONE
-      };
-
-    val in_strm =
-      BinIO.mkInstream (
-        BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
-
-    val out_strm =
-      BinIO.mkOutstream (
-        BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
-
-    in (in_strm, out_strm) end;
-
-end;
-