Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
some partial workarounds for Cygwin;

--- a/bin/isabelle-process	Mon Aug 09 13:56:02 2010 +0200
+++ b/bin/isabelle-process	Mon Aug 09 18:18:32 2010 +0200
@@ -29,8 +29,8 @@
   echo "    -I           startup Isar interaction mode"
   echo "    -P           startup Proof General interaction mode"
   echo "    -S           secure mode -- disallow critical operations"
+  echo "    -W IN:OUT    startup process wrapper, with input/output fifos"
   echo "    -X           startup PGIP interaction mode"
-  echo "    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream"
   echo "    -e MLTEXT    pass MLTEXT to the ML session"
   echo "    -f           pass 'Session.finish();' to the ML session"
   echo "    -m MODE      add print mode for output"
@@ -61,7 +61,7 @@
 ISAR=false
 PROOFGENERAL=""
 SECURE=""
-WRAPPER_OUTPUT=""
+WRAPPER_FIFOS=""
 PGIP=""
 MLTEXT=""
 MODES=""
@@ -82,7 +82,7 @@
       SECURE=true
       ;;
     W)
-      WRAPPER_OUTPUT="$OPTARG"
+      WRAPPER_FIFOS="$OPTARG"
       ;;
     X)
       PGIP=true
@@ -212,9 +212,13 @@
 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
 
 NICE="nice"
-if [ -n "$WRAPPER_OUTPUT" ]; then
-  [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
-  MLTEXT="$MLTEXT; Isabelle_Process.init \"$WRAPPER_OUTPUT\";"
+
+if [ -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]}\";"
 elif [ -n "$PGIP" ]; then
   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
 elif [ -n "$PROOFGENERAL" ]; then

--- a/doc-src/System/Thy/Basics.thy	Mon Aug 09 13:56:02 2010 +0200
+++ b/doc-src/System/Thy/Basics.thy	Mon Aug 09 18:18:32 2010 +0200
@@ -331,7 +331,7 @@
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
-    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
+    -W IN:OUT    startup process wrapper, with input/output fifos
     -X           startup PGIP interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
     -f           pass 'Session.finish();' to the ML session
@@ -406,12 +406,13 @@
   interaction mode on startup, instead of the primitive ML top-level.
   The @{verbatim "-P"} option configures the top-level loop for
   interaction with the Proof General user interface, and the
-  @{verbatim "-X"} option enables XML-based PGIP communication.  The
-  @{verbatim "-W"} option makes Isabelle enter a special process
-  wrapper for interaction via an external program; the protocol is a
-  stripped-down version of Proof General the interaction mode, see
-  also @{"file" "~~/src/Pure/System/isabelle_process.ML"} and @{"file"
-  "~~/src/Pure/System/isabelle_process.scala"}.
+  @{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 "-S"} option makes the Isabelle process more
   secure by disabling some critical operations, notably runtime

--- a/doc-src/System/Thy/document/Basics.tex	Mon Aug 09 13:56:02 2010 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Mon Aug 09 18:18:32 2010 +0200
@@ -344,7 +344,7 @@
     -I           startup Isar interaction mode
     -P           startup Proof General interaction mode
     -S           secure mode -- disallow critical operations
-    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
+    -W IN:OUT    startup process wrapper, with input/output fifos
     -X           startup PGIP interaction mode
     -e MLTEXT    pass MLTEXT to the ML session
     -f           pass 'Session.finish();' to the ML session
@@ -419,11 +419,13 @@
   interaction mode on startup, instead of the primitive ML top-level.
   The \verb|-P| option configures the top-level loop for
   interaction with the Proof General user interface, and the
-  \verb|-X| option enables XML-based PGIP communication.  The
-  \verb|-W| option makes Isabelle enter a special process
-  wrapper for interaction via an external program; the protocol is a
-  stripped-down version of Proof General the interaction mode, see
-  also \hyperlink{file.~~/src/Pure/System/isabelle-process.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}ML}}}} and \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}.
+  \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 \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}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

--- a/lib/Tools/mkfifo	Mon Aug 09 13:56:02 2010 +0200
+++ b/lib/Tools/mkfifo	Mon Aug 09 18:18:32 2010 +0200
@@ -28,6 +28,8 @@
 
 [ "$#" != 0 ] && usage
 
+#FIXME potential race condition wrt. future processes with same pid
 FIFO="/tmp/isabelle-fifo$$"
-mkfifo -m 600 "$FIFO" || fail "Failed to create named pipe $FIFO"
+
+mkfifo -m 600 "$FIFO" || fail "Failed to create fifo: $FIFO"
 echo "$FIFO"

--- a/src/Pure/General/source.ML	Mon Aug 09 13:56:02 2010 +0200
+++ b/src/Pure/General/source.ML	Mon Aug 09 18:18:32 2010 +0200
@@ -19,7 +19,7 @@
   val exhausted: ('a, 'b) source -> ('a, 'a list) source
   val of_string: string -> (string, string list) source
   val of_string_limited: int -> string -> (string, substring) source
-  val tty: (string, unit) source
+  val tty: TextIO.instream -> (string, unit) source
   val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
     (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
     ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
@@ -129,11 +129,11 @@
       | SOME _ => TextIO.input instream :: slurp ());
   in maps explode (slurp ()) end;
 
-val tty = make_source [] () default_prompt (fn prompt => fn () =>
-  let val input = slurp_input TextIO.stdIn in
+fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () =>
+  let val input = slurp_input in_stream in
     if exists (fn c => c = "\n") input then (input, ())
     else
-      (case (Output.prompt prompt; TextIO.inputLine TextIO.stdIn) of
+      (case (Output.prompt prompt; TextIO.inputLine in_stream) of
         SOME line => (input @ explode line, ())
       | NONE => (input, ()))
   end);

--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 09 13:56:02 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 09 18:18:32 2010 +0200
@@ -29,7 +29,7 @@
   val parse: Position.T -> string -> Toplevel.transition list
   val process_file: Path.T -> theory -> theory
   type isar
-  val isar: bool -> isar
+  val isar: TextIO.instream -> bool -> isar
   val prepare_command: Position.T -> string -> Toplevel.transition
   val load_thy: string -> (unit -> theory) -> Position.T -> string -> (unit -> unit) * theory
 end;
@@ -222,8 +222,8 @@
   Source.source) Source.source) Source.source) Source.source)
   Source.source) Source.source) Source.source) Source.source;
 
-fun isar term : isar =
-  Source.tty
+fun isar in_stream term : isar =
+  Source.tty in_stream
   |> Symbol.source {do_recover = true}
   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   |> toplevel_source term (SOME true) get_command;

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 09 13:56:02 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 09 18:18:32 2010 +0200
@@ -245,7 +245,8 @@
         sync_thy_loader ();
        Unsynchronized.change print_mode (update (op =) proof_generalN);
        Secure.PG_setup ();
-       Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
+       Isar.toplevel_loop TextIO.stdIn
+        {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
 
 (* fake old ThyLoad -- with new semantics *)

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 09 13:56:02 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 09 18:18:32 2010 +0200
@@ -1000,7 +1000,8 @@
 
   val xmlP = XML.parse_comments |-- XML.parse_element >> single
 
-  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
+  val tty_src =
+    Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE (Source.tty TextIO.stdIn))
 
   fun pgip_toplevel x = loop true x
 end

--- a/src/Pure/System/isabelle_process.ML	Mon Aug 09 13:56:02 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Aug 09 18:18:32 2010 +0200
@@ -11,7 +11,7 @@
 signature ISABELLE_PROCESS =
 sig
   val isabelle_processN: string
-  val init: string -> unit
+  val init: string -> string -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
@@ -60,13 +60,19 @@
       (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
   in loop end;
 
+fun rendezvous f fifo =
+  let
+    val path = File.platform_path (Path.explode fifo);
+    val result = f fifo;  (*block until peer is ready*)
+    val _ = OS.FileSys.remove path;  (*ready; prevent future access -- potential race condition*)
+  in result end;
+
 in
 
-fun setup_channels out =
+fun setup_channels in_fifo out_fifo =
   let
-    val path = File.platform_path (Path.explode out);
-    val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
-    val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
+    val in_stream = rendezvous TextIO.openIn in_fifo;
+    val out_stream = rendezvous TextIO.openOut out_fifo;
     val _ = Simple_Thread.fork false (auto_flush out_stream);
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
@@ -80,7 +86,7 @@
     Output.debug_fn    := standard_message out_stream "H";
     Output.priority_fn := ! Output.writeln_fn;
     Output.prompt_fn   := ignore;
-    out_stream
+    (in_stream, out_stream)
   end;
 
 end;
@@ -88,13 +94,15 @@
 
 (* init *)
 
-fun init out =
- (Unsynchronized.change print_mode
-    (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
-  setup_channels out |> init_message;
-  quick_and_dirty := true;  (* FIXME !? *)
-  Keyword.status ();
-  Output.status (Markup.markup Markup.ready "");
-  Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
+fun init in_fifo out_fifo =
+  let
+    val _ = Unsynchronized.change print_mode
+      (fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+    val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
+    val _ = init_message out_stream;
+    val _ = quick_and_dirty := true;  (* FIXME !? *)
+    val _ = Keyword.status ();
+    val _ = Output.status (Markup.markup Markup.ready "");
+  in Isar.toplevel_loop in_stream {init = true, welcome = false, sync = true, secure = true} end;
 
 end;

--- a/src/Pure/System/isabelle_process.scala	Mon Aug 09 13:56:02 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Aug 09 18:18:32 2010 +0200
@@ -178,11 +178,14 @@
   }
 
 
-  /* stdin */
+  /* commands */
 
-  private class Stdin_Thread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
-    override def run() = {
-      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Standard_System.charset))
+  private class Command_Thread(fifo: String) extends Thread("isabelle: commands")
+  {
+    override def run()
+    {
+      val stream = system.fifo_output_stream(fifo)
+      val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
       var finished = false
       while (!finished) {
         try {
@@ -200,19 +203,21 @@
           //}}}
         }
         catch {
-          case e: IOException => put_result(Markup.SYSTEM, "Stdin thread: " + e.getMessage)
+          case e: IOException => put_result(Markup.SYSTEM, "Command thread: " + e.getMessage)
         }
       }
-      put_result(Markup.SYSTEM, "Stdin thread terminated")
+      put_result(Markup.SYSTEM, "Command thread terminated")
     }
   }
 
 
-  /* stdout */
+  /* raw stdout */
 
-  private class Stdout_Thread(in_stream: InputStream) extends Thread("isabelle: stdout") {
-    override def run() = {
-      val reader = new BufferedReader(new InputStreamReader(in_stream, Standard_System.charset))
+  private class Stdout_Thread(stream: InputStream) extends Thread("isabelle: stdout")
+  {
+    override def run() =
+    {
+      val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
       var result = new StringBuilder(100)
 
       var finished = false
@@ -253,7 +258,7 @@
     private class Protocol_Error(msg: String) extends Exception(msg)
     override def run()
     {
-      val stream = system.fifo_stream(fifo)
+      val stream = system.fifo_input_stream(fifo)
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
@@ -329,43 +334,44 @@
   /** main **/
 
   {
-    /* messages */
+    /* private communication channels */
 
-    val message_fifo = system.mk_fifo()
-    def rm_fifo() = system.rm_fifo(message_fifo)
+    val in_fifo = system.mk_fifo()
+    val out_fifo = system.mk_fifo()
+    def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
 
-    val message_thread = new Message_Thread(message_fifo)
+    val command_thread = new Command_Thread(in_fifo)
+    val message_thread = new Message_Thread(out_fifo)
+
+    command_thread.start
     message_thread.start
 
 
     /* exec process */
 
     try {
-      val cmdline = List(system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
+      val cmdline =
+        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
       proc = system.execute(true, cmdline: _*)
     }
     catch {
       case e: IOException =>
-        rm_fifo()
+        rm_fifos()
         error("Failed to execute Isabelle process: " + e.getMessage)
     }
-
-
-    /* stdin/stdout */
-
-    new Stdin_Thread(proc.getOutputStream).start
     new Stdout_Thread(proc.getInputStream).start
 
 
     /* exit */
 
     new Thread("isabelle: exit") {
-      override def run() = {
+      override def run()
+      {
         val rc = proc.waitFor()
         Thread.sleep(300)  // FIXME property!?
         put_result(Markup.SYSTEM, "Exit thread terminated")
         put_result(Markup.EXIT, rc.toString)
-        rm_fifo()
+        rm_fifos()
       }
     }.start
   }

--- a/src/Pure/System/isabelle_system.scala	Mon Aug 09 13:56:02 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Aug 09 18:18:32 2010 +0200
@@ -8,9 +8,8 @@
 
 import java.util.regex.Pattern
 import java.util.Locale
-import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
-  BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
-  File, IOException}
+import java.io.{BufferedInputStream, FileInputStream, BufferedOutputStream, FileOutputStream,
+  OutputStream, File, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 import java.awt.font.TextAttribute
 
@@ -288,11 +287,12 @@
     if (rc != 0) error(result)
   }
 
-  def fifo_stream(fifo: String): BufferedInputStream =
+  def fifo_input_stream(fifo: String): BufferedInputStream =
   {
-    // blocks until writer is ready
+    // block until peer is ready
     val stream =
       if (Platform.is_windows) {
+        // Cygwin fifo as Windows/Java input stream
         val proc = execute(false, "cat", fifo)
         proc.getOutputStream.close
         proc.getErrorStream.close
@@ -302,6 +302,34 @@
     new BufferedInputStream(stream)
   }
 
+  def fifo_output_stream(fifo: String): BufferedOutputStream =
+  {
+    // block until peer is ready
+    val stream =
+      if (Platform.is_windows) {
+        // Cygwin fifo as Windows/Java output stream (beware of buffering)
+        // FIXME FIXME FIXME
+        val script =
+          "open(FIFO, \">" + fifo + "\") || die $!; my $buffer; " +
+          "while ((sysread STDIN, $buffer, 65536), length $buffer > 0)" +
+          " { syswrite FIFO, $buffer; }; close FIFO;"
+        val proc = execute(false, "perl", "-e", script)
+        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) }
+        }
+        proc.getOutputStream
+      }
+      else new FileOutputStream(fifo)
+    new BufferedOutputStream(stream)
+  }
+
 
 
   /** Isabelle resources **/

--- a/src/Pure/System/isar.ML	Mon Aug 09 13:56:02 2010 +0200
+++ b/src/Pure/System/isar.ML	Mon Aug 09 18:18:32 2010 +0200
@@ -18,7 +18,8 @@
   val kill: unit -> unit
   val kill_proof: unit -> unit
   val crashes: exn list Unsynchronized.ref
-  val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
+  val toplevel_loop: TextIO.instream ->
+    {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   val loop: unit -> unit
   val main: unit -> unit
 end;
@@ -131,20 +132,22 @@
 
 in
 
-fun toplevel_loop {init = do_init, welcome, sync, secure} =
+fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
   Secure.Isar_setup ();
   if do_init then init () else ();
   if welcome then writeln (Session.welcome ()) else ();
-  uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ());
+  uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
 
 end;
 
 fun loop () =
-  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
+  toplevel_loop TextIO.stdIn
+    {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
 
 fun main () =
-  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
+  toplevel_loop TextIO.stdIn
+    {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};