--- 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
--- 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
--- 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
--- 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
--- /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;
+
--- 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 \
--- 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;
+
--- 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";
--- 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;
--- 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()
}
--- 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 **/
--- /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;
+
--- /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 }
+}
--- 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
--- 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
--- 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";
--- 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);
--- /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;
+
--- 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;
-