always use sockets on Windows/Cygwin;
authorwenzelm
Mon Oct 17 11:24:22 2011 +0200 (2011-10-17 ago)
changeset 45158db4bf4fb5492
parent 45157 efc2e2d80218
child 45161 699848baf70b
always use sockets on Windows/Cygwin;
discontinued special raw_dump facility;
lib/scripts/raw_dump
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Pure/System/system_channel.ML
src/Pure/System/system_channel.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/lib/scripts/raw_dump	Sun Oct 16 21:49:47 2011 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,56 +0,0 @@
     1.4 -#!/usr/bin/env perl
     1.5 -#
     1.6 -# Author: Makarius
     1.7 -#
     1.8 -# raw_dump - direct copy without extra buffering
     1.9 -#
    1.10 -
    1.11 -use warnings;
    1.12 -use strict;
    1.13 -
    1.14 -use IO::File;
    1.15 -
    1.16 -
    1.17 -# args
    1.18 -
    1.19 -my ($input, $output) = @ARGV;
    1.20 -
    1.21 -
    1.22 -# prepare files
    1.23 -
    1.24 -my $infile;
    1.25 -my $outfile;
    1.26 -
    1.27 -if ($input eq "-") { $infile = *STDIN; }
    1.28 -else {
    1.29 -  $infile = new IO::File $input, "r";
    1.30 -  defined $infile || die $!;
    1.31 -}
    1.32 -
    1.33 -if ($output eq "-") { $outfile = *STDOUT; }
    1.34 -else {
    1.35 -  $outfile = new IO::File $output, "w";
    1.36 -  defined $outfile || die $!;
    1.37 -}
    1.38 -
    1.39 -binmode $infile;
    1.40 -binmode $outfile;
    1.41 -
    1.42 -
    1.43 -# main loop
    1.44 -
    1.45 -my $chunk;
    1.46 -while ((sysread $infile, $chunk, 65536), length $chunk > 0) {
    1.47 -  my $end = length $chunk;
    1.48 -  my $offset = 0;
    1.49 -  while ($offset < $end) {
    1.50 -    $offset += syswrite $outfile, $chunk, $end - $offset, $offset;
    1.51 -  }
    1.52 -}
    1.53 -
    1.54 -
    1.55 -# cleanup
    1.56 -
    1.57 -undef $infile;
    1.58 -undef $outfile;
    1.59 -
     2.1 --- a/src/Pure/System/isabelle_process.ML	Sun Oct 16 21:49:47 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Oct 17 11:24:22 2011 +0200
     2.3 @@ -10,9 +10,9 @@
     2.4    .. stdin/stdout/stderr freely available (raw ML loop)
     2.5    .. protocol thread initialization
     2.6    ... rendezvous on system channel
     2.7 -  ... out_fifo INIT(pid): channels ready
     2.8 -  ... out_fifo STATUS(keywords)
     2.9 -  ... out_fifo READY: main loop ready
    2.10 +  ... message INIT(pid): channels ready
    2.11 +  ... message STATUS(keywords)
    2.12 +  ... message READY: main loop ready
    2.13  *)
    2.14  
    2.15  signature ISABELLE_PROCESS =
     3.1 --- a/src/Pure/System/isabelle_process.scala	Sun Oct 16 21:49:47 2011 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Oct 17 11:24:22 2011 +0200
     3.3 @@ -77,7 +77,6 @@
     3.4  
     3.5  class Isabelle_Process(
     3.6      timeout: Time = Time.seconds(25),
     3.7 -    use_socket: Boolean = false,
     3.8      receiver: Isabelle_Process.Message => Unit = Console.println(_),
     3.9      args: List[String] = Nil)
    3.10  {
    3.11 @@ -130,7 +129,7 @@
    3.12  
    3.13    /** process manager **/
    3.14  
    3.15 -  private val system_channel = System_Channel(use_socket)
    3.16 +  private val system_channel = System_Channel()
    3.17  
    3.18    private val process =
    3.19      try {
     4.1 --- a/src/Pure/System/session.scala	Sun Oct 16 21:49:47 2011 +0200
     4.2 +++ b/src/Pure/System/session.scala	Mon Oct 17 11:24:22 2011 +0200
     4.3 @@ -137,7 +137,7 @@
     4.4  
     4.5    /* actor messages */
     4.6  
     4.7 -  private case class Start(timeout: Time, use_socket: Boolean, args: List[String])
     4.8 +  private case class Start(timeout: Time, args: List[String])
     4.9    private case object Cancel_Execution
    4.10    private case class Init_Node(name: Document.Node.Name,
    4.11      header: Document.Node_Header, perspective: Text.Perspective, text: String)
    4.12 @@ -405,12 +405,11 @@
    4.13        receiveWithin(commands_changed_delay.flush_timeout) {
    4.14          case TIMEOUT => commands_changed_delay.flush()
    4.15  
    4.16 -        case Start(timeout, use_socket, args) if prover.isEmpty =>
    4.17 +        case Start(timeout, args) if prover.isEmpty =>
    4.18            if (phase == Session.Inactive || phase == Session.Failed) {
    4.19              phase = Session.Startup
    4.20              prover =
    4.21 -              Some(new Isabelle_Process(timeout, use_socket, receiver.invoke _, args)
    4.22 -                with Isar_Document)
    4.23 +              Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isar_Document)
    4.24            }
    4.25  
    4.26          case Stop =>
    4.27 @@ -469,10 +468,10 @@
    4.28  
    4.29    /* actions */
    4.30  
    4.31 -  def start(timeout: Time, use_socket: Boolean, args: List[String])
    4.32 -  { session_actor ! Start(timeout, use_socket, args) }
    4.33 +  def start(timeout: Time, args: List[String])
    4.34 +  { session_actor ! Start(timeout, args) }
    4.35  
    4.36 -  def start(args: List[String]) { start (Time.seconds(25), false, args) }
    4.37 +  def start(args: List[String]) { start (Time.seconds(25), args) }
    4.38  
    4.39    def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
    4.40  
     5.1 --- a/src/Pure/System/system_channel.ML	Sun Oct 16 21:49:47 2011 +0200
     5.2 +++ b/src/Pure/System/system_channel.ML	Mon Oct 17 11:24:22 2011 +0200
     5.3 @@ -47,7 +47,7 @@
     5.4    end;
     5.5  
     5.6  
     5.7 -(* sockets *)  (* FIXME raw unbuffered IO !?!? *)
     5.8 +(* sockets *)  (* FIXME proper buffering via BinIO (after Poly/ML 5.4.1) *)
     5.9  
    5.10  local
    5.11  
     6.1 --- a/src/Pure/System/system_channel.scala	Sun Oct 16 21:49:47 2011 +0200
     6.2 +++ b/src/Pure/System/system_channel.scala	Mon Oct 17 11:24:22 2011 +0200
     6.3 @@ -15,7 +15,7 @@
     6.4  object System_Channel
     6.5  {
     6.6    def apply(use_socket: Boolean = false): System_Channel =
     6.7 -    if (use_socket) new Socket_Channel else new Fifo_Channel
     6.8 +    if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
     6.9  }
    6.10  
    6.11  abstract class System_Channel
    6.12 @@ -52,35 +52,14 @@
    6.13  
    6.14    private def fifo_input_stream(fifo: String): InputStream =
    6.15    {
    6.16 -    if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
    6.17 -      val proc =
    6.18 -        Isabelle_System.execute(false,
    6.19 -          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-")
    6.20 -      proc.getOutputStream.close
    6.21 -      proc.getErrorStream.close
    6.22 -      proc.getInputStream
    6.23 -    }
    6.24 -    else new FileInputStream(fifo)
    6.25 +    require(!Platform.is_windows)
    6.26 +    new FileInputStream(fifo)
    6.27    }
    6.28  
    6.29    private def fifo_output_stream(fifo: String): OutputStream =
    6.30    {
    6.31 -    if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
    6.32 -      val proc =
    6.33 -        Isabelle_System.execute(false,
    6.34 -          Isabelle_System.standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo)
    6.35 -      proc.getInputStream.close
    6.36 -      proc.getErrorStream.close
    6.37 -      val out = proc.getOutputStream
    6.38 -      new OutputStream {
    6.39 -        override def close() { out.close(); proc.waitFor() }
    6.40 -        override def flush() { out.flush() }
    6.41 -        override def write(b: Array[Byte]) { out.write(b) }
    6.42 -        override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
    6.43 -        override def write(b: Int) { out.write(b) }
    6.44 -      }
    6.45 -    }
    6.46 -    else new FileOutputStream(fifo)
    6.47 +    require(!Platform.is_windows)
    6.48 +    new FileOutputStream(fifo)
    6.49    }
    6.50  
    6.51  
     7.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 16 21:49:47 2011 +0200
     7.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Oct 17 11:24:22 2011 +0200
     7.3 @@ -36,15 +36,6 @@
     7.4  )
     7.5  
     7.6  
     7.7 -## defaults
     7.8 -
     7.9 -if [ "$OSTYPE" = cygwin ]; then
    7.10 -  SOCKET_DEFAULT="true"
    7.11 -else
    7.12 -  SOCKET_DEFAULT="false"
    7.13 -fi
    7.14 -
    7.15 -
    7.16  ## diagnostics
    7.17  
    7.18  PRG="$(basename "$0")"
    7.19 @@ -57,7 +48,6 @@
    7.20    echo "  Options are:"
    7.21    echo "    -J OPTION    add JVM runtime option"
    7.22    echo "                 (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
    7.23 -  echo "    -S BOOL      enable socket communication instead of fifos (default: $SOCKET_DEFAULT)"
    7.24    echo "    -b           build only"
    7.25    echo "    -d           enable debugger"
    7.26    echo "    -f           fresh build"
    7.27 @@ -78,11 +68,6 @@
    7.28    exit 2
    7.29  }
    7.30  
    7.31 -function check_bool()
    7.32 -{
    7.33 -  [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
    7.34 -}
    7.35 -
    7.36  function failed()
    7.37  {
    7.38    fail "Failed!"
    7.39 @@ -95,23 +80,18 @@
    7.40  
    7.41  BUILD_ONLY=false
    7.42  BUILD_JARS="jars"
    7.43 -JEDIT_USE_SOCKET="$SOCKET_DEFAULT"
    7.44  JEDIT_LOGIC="$ISABELLE_LOGIC"
    7.45  JEDIT_PRINT_MODE=""
    7.46  
    7.47  function getoptions()
    7.48  {
    7.49    OPTIND=1
    7.50 -  while getopts "J:S:bdfj:l:m:" OPT
    7.51 +  while getopts "J:bdfj:l:m:" OPT
    7.52    do
    7.53      case "$OPT" in
    7.54        J)
    7.55          JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
    7.56          ;;
    7.57 -      S)
    7.58 -        check_bool "$OPTARG"
    7.59 -        JEDIT_USE_SOCKET="$OPTARG"
    7.60 -        ;;
    7.61        b)
    7.62          BUILD_ONLY=true
    7.63          ;;
    7.64 @@ -310,7 +290,7 @@
    7.65        ;;
    7.66    esac
    7.67  
    7.68 -  export JEDIT_USE_SOCKET JEDIT_LOGIC JEDIT_PRINT_MODE
    7.69 +  export JEDIT_LOGIC JEDIT_PRINT_MODE
    7.70  
    7.71    exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
    7.72      -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
     8.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Oct 16 21:49:47 2011 +0200
     8.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Oct 17 11:24:22 2011 +0200
     8.3 @@ -320,14 +320,13 @@
     8.4    def start_session()
     8.5    {
     8.6      val timeout = Time_Property("startup-timeout", Time.seconds(25)) max Time.seconds(5)
     8.7 -    val use_socket = Isabelle_System.getenv("JEDIT_USE_SOCKET") == "true"
     8.8      val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     8.9      val logic = {
    8.10        val logic = Property("logic")
    8.11        if (logic != null && logic != "") logic
    8.12        else Isabelle.default_logic()
    8.13      }
    8.14 -    session.start(timeout, use_socket, modes ::: List(logic))
    8.15 +    session.start(timeout, modes ::: List(logic))
    8.16    }
    8.17  
    8.18