# HG changeset patch
# User wenzelm
# Date 1318867514 -7200
# Node ID 699848baf70b2346bdcf47bb46dbe7d4affdef06
# Parent  b09575e075a52ef4d489c47c8e2501e3f321ab89# Parent  db4bf4fb549219a8616c0b8c8d9630a4b2a1b770
merged

diff -r b09575e075a5 -r 699848baf70b lib/scripts/raw_dump
--- a/lib/scripts/raw_dump	Mon Oct 17 14:22:14 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Makarius
-#
-# raw_dump - direct copy without extra buffering
-#
-
-use warnings;
-use strict;
-
-use IO::File;
-
-
-# args
-
-my ($input, $output) = @ARGV;
-
-
-# prepare files
-
-my $infile;
-my $outfile;
-
-if ($input eq "-") { $infile = *STDIN; }
-else {
-  $infile = new IO::File $input, "r";
-  defined $infile || die $!;
-}
-
-if ($output eq "-") { $outfile = *STDOUT; }
-else {
-  $outfile = new IO::File $output, "w";
-  defined $outfile || die $!;
-}
-
-binmode $infile;
-binmode $outfile;
-
-
-# main loop
-
-my $chunk;
-while ((sysread $infile, $chunk, 65536), length $chunk > 0) {
-  my $end = length $chunk;
-  my $offset = 0;
-  while ($offset < $end) {
-    $offset += syswrite $outfile, $chunk, $end - $offset, $offset;
-  }
-}
-
-
-# cleanup
-
-undef $infile;
-undef $outfile;
-
diff -r b09575e075a5 -r 699848baf70b src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Oct 17 14:22:14 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Oct 17 18:05:14 2011 +0200
@@ -10,9 +10,9 @@
   .. stdin/stdout/stderr freely available (raw ML loop)
   .. protocol thread initialization
   ... rendezvous on system channel
-  ... out_fifo INIT(pid): channels ready
-  ... out_fifo STATUS(keywords)
-  ... out_fifo READY: main loop ready
+  ... message INIT(pid): channels ready
+  ... message STATUS(keywords)
+  ... message READY: main loop ready
 *)
 
 signature ISABELLE_PROCESS =
diff -r b09575e075a5 -r 699848baf70b src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Oct 17 14:22:14 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Oct 17 18:05:14 2011 +0200
@@ -77,7 +77,6 @@
 
 class Isabelle_Process(
     timeout: Time = Time.seconds(25),
-    use_socket: Boolean = false,
     receiver: Isabelle_Process.Message => Unit = Console.println(_),
     args: List[String] = Nil)
 {
@@ -130,7 +129,7 @@
 
   /** process manager **/
 
-  private val system_channel = System_Channel(use_socket)
+  private val system_channel = System_Channel()
 
   private val process =
     try {
diff -r b09575e075a5 -r 699848baf70b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Oct 17 14:22:14 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Oct 17 18:05:14 2011 +0200
@@ -137,7 +137,7 @@
 
   /* actor messages */
 
-  private case class Start(timeout: Time, use_socket: Boolean, args: List[String])
+  private case class Start(timeout: Time, args: List[String])
   private case object Cancel_Execution
   private case class Init_Node(name: Document.Node.Name,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)
@@ -405,12 +405,11 @@
       receiveWithin(commands_changed_delay.flush_timeout) {
         case TIMEOUT => commands_changed_delay.flush()
 
-        case Start(timeout, use_socket, args) if prover.isEmpty =>
+        case Start(timeout, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
             prover =
-              Some(new Isabelle_Process(timeout, use_socket, receiver.invoke _, args)
-                with Isar_Document)
+              Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isar_Document)
           }
 
         case Stop =>
@@ -469,10 +468,10 @@
 
   /* actions */
 
-  def start(timeout: Time, use_socket: Boolean, args: List[String])
-  { session_actor ! Start(timeout, use_socket, args) }
+  def start(timeout: Time, args: List[String])
+  { session_actor ! Start(timeout, args) }
 
-  def start(args: List[String]) { start (Time.seconds(25), false, args) }
+  def start(args: List[String]) { start (Time.seconds(25), args) }
 
   def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
 
diff -r b09575e075a5 -r 699848baf70b src/Pure/System/system_channel.ML
--- a/src/Pure/System/system_channel.ML	Mon Oct 17 14:22:14 2011 +0200
+++ b/src/Pure/System/system_channel.ML	Mon Oct 17 18:05:14 2011 +0200
@@ -47,7 +47,7 @@
   end;
 
 
-(* sockets *)  (* FIXME raw unbuffered IO !?!? *)
+(* sockets *)  (* FIXME proper buffering via BinIO (after Poly/ML 5.4.1) *)
 
 local
 
diff -r b09575e075a5 -r 699848baf70b src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Mon Oct 17 14:22:14 2011 +0200
+++ b/src/Pure/System/system_channel.scala	Mon Oct 17 18:05:14 2011 +0200
@@ -15,7 +15,7 @@
 object System_Channel
 {
   def apply(use_socket: Boolean = false): System_Channel =
-    if (use_socket) new Socket_Channel else new Fifo_Channel
+    if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
 }
 
 abstract class System_Channel
@@ -52,35 +52,14 @@
 
   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)
+    require(!Platform.is_windows)
+    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)
+    require(!Platform.is_windows)
+    new FileOutputStream(fifo)
   }
 
 
diff -r b09575e075a5 -r 699848baf70b src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Oct 17 14:22:14 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Oct 17 18:05:14 2011 +0200
@@ -36,15 +36,6 @@
 )
 
 
-## defaults
-
-if [ "$OSTYPE" = cygwin ]; then
-  SOCKET_DEFAULT="true"
-else
-  SOCKET_DEFAULT="false"
-fi
-
-
 ## diagnostics
 
 PRG="$(basename "$0")"
@@ -57,7 +48,6 @@
   echo "  Options are:"
   echo "    -J OPTION    add JVM runtime option"
   echo "                 (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
-  echo "    -S BOOL      enable socket communication instead of fifos (default: $SOCKET_DEFAULT)"
   echo "    -b           build only"
   echo "    -d           enable debugger"
   echo "    -f           fresh build"
@@ -78,11 +68,6 @@
   exit 2
 }
 
-function check_bool()
-{
-  [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
-}
-
 function failed()
 {
   fail "Failed!"
@@ -95,23 +80,18 @@
 
 BUILD_ONLY=false
 BUILD_JARS="jars"
-JEDIT_USE_SOCKET="$SOCKET_DEFAULT"
 JEDIT_LOGIC="$ISABELLE_LOGIC"
 JEDIT_PRINT_MODE=""
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "J:S:bdfj:l:m:" OPT
+  while getopts "J:bdfj:l:m:" OPT
   do
     case "$OPT" in
       J)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
         ;;
-      S)
-        check_bool "$OPTARG"
-        JEDIT_USE_SOCKET="$OPTARG"
-        ;;
       b)
         BUILD_ONLY=true
         ;;
@@ -310,7 +290,7 @@
       ;;
   esac
 
-  export JEDIT_USE_SOCKET JEDIT_LOGIC JEDIT_PRINT_MODE
+  export JEDIT_LOGIC JEDIT_PRINT_MODE
 
   exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
     -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
diff -r b09575e075a5 -r 699848baf70b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Oct 17 14:22:14 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Oct 17 18:05:14 2011 +0200
@@ -320,14 +320,13 @@
   def start_session()
   {
     val timeout = Time_Property("startup-timeout", Time.seconds(25)) max Time.seconds(5)
-    val use_socket = Isabelle_System.getenv("JEDIT_USE_SOCKET") == "true"
     val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     val logic = {
       val logic = Property("logic")
       if (logic != null && logic != "") logic
       else Isabelle.default_logic()
     }
-    session.start(timeout, use_socket, modes ::: List(logic))
+    session.start(timeout, modes ::: List(logic))
   }