--- 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;
-
--- 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 =
--- 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 {
--- 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 }
--- 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
--- 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)
}
--- 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")" \
--- 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))
}