--- a/bin/isabelle-process Fri Sep 23 16:44:51 2011 +0200
+++ b/bin/isabelle-process Fri Sep 23 16:50:39 2011 +0200
@@ -212,7 +212,7 @@
ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
-[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
+[ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
[ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Sep 23 16:44:51 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Sep 23 16:50:39 2011 +0200
@@ -1270,7 +1270,7 @@
lemma correct_state_impl_Some_method:
"G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>
\<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
-by (auto simp add: correct_state_def Let_def)
+by (auto simp add: correct_state_def)
lemma BV_correct_1 [rule_format]:
--- a/src/Pure/Syntax/syntax_trans.ML Fri Sep 23 16:44:51 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Fri Sep 23 16:50:39 2011 +0200
@@ -12,7 +12,11 @@
signature SYNTAX_TRANS =
sig
include BASIC_SYNTAX_TRANS
+ val bracketsN: string
+ val no_bracketsN: string
val no_brackets: unit -> bool
+ val type_bracketsN: string
+ val no_type_bracketsN: string
val no_type_brackets: unit -> bool
val abs_tr: term list -> term
val mk_binder_tr: string * string -> string * (term list -> term)
--- a/src/Pure/System/isabelle_process.ML Fri Sep 23 16:44:51 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML Fri Sep 23 16:50:39 2011 +0200
@@ -179,8 +179,10 @@
val _ = Context.set_thread_data NONE;
val _ =
Unsynchronized.change print_mode
- (fold (update op =)
- [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+ (fn mode =>
+ (mode @ [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN])
+ |> fold (update op =)
+ [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
val channel = rendezvous ();
val _ = setup_channels channel;
--- a/src/Pure/System/isabelle_process.scala Fri Sep 23 16:44:51 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala Fri Sep 23 16:50:39 2011 +0200
@@ -75,16 +75,15 @@
}
-class Isabelle_Process(timeout: Time, receiver: Isabelle_Process.Message => Unit, args: String*)
+class Isabelle_Process(
+ timeout: Time = Time.seconds(10),
+ use_socket: Boolean = false,
+ receiver: Isabelle_Process.Message => Unit = Console.println(_),
+ args: List[String] = Nil)
{
import Isabelle_Process._
- /* demo constructor */
-
- def this(args: String*) = this(Time.seconds(10), Console.println(_), args: _*)
-
-
/* results */
private def system_result(text: String)
@@ -131,13 +130,13 @@
/** process manager **/
- private val system_channel = System_Channel()
+ private val system_channel = System_Channel(use_socket)
private val process =
try {
val cmdline =
Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
- (system_channel.isabelle_args ::: args.toList)
+ (system_channel.isabelle_args ::: args)
new Isabelle_System.Managed_Process(true, cmdline: _*)
}
catch { case e: IOException => system_channel.accepted(); throw(e) }
--- a/src/Pure/System/session.scala Fri Sep 23 16:44:51 2011 +0200
+++ b/src/Pure/System/session.scala Fri Sep 23 16:50:39 2011 +0200
@@ -137,7 +137,7 @@
/* actor messages */
- private case class Start(timeout: Time, args: List[String])
+ private case class Start(timeout: Time, use_socket: Boolean, 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,11 +405,12 @@
receiveWithin(commands_changed_delay.flush_timeout) {
case TIMEOUT => commands_changed_delay.flush()
- case Start(timeout, args) if prover.isEmpty =>
+ case Start(timeout, use_socket, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
prover =
- Some(new Isabelle_Process(timeout, receiver.invoke _, args:_*) with Isar_Document)
+ Some(new Isabelle_Process(timeout, use_socket, receiver.invoke _, args)
+ with Isar_Document)
}
case Stop =>
@@ -468,7 +469,8 @@
/* actions */
- def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
+ def start(timeout: Time = Time.seconds(10), use_socket: Boolean = false, args: List[String])
+ { session_actor ! Start(timeout, use_socket, args) }
def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
--- a/src/Pure/System/system_channel.ML Fri Sep 23 16:44:51 2011 +0200
+++ b/src/Pure/System/system_channel.ML Fri Sep 23 16:50:39 2011 +0200
@@ -47,31 +47,65 @@
end;
-(* sockets *)
+(* sockets *) (* FIXME raw unbuffered IO !?!? *)
+
+local
-fun read_line in_stream =
+fun readN socket n =
let
- fun result cs = String.implode (rev (#"\n" :: cs));
+ fun read i buf =
+ let
+ val s = Byte.bytesToString (Socket.recvVec (socket, n - i));
+ val m = size s;
+ val i' = i + m;
+ val buf' = Buffer.add s buf;
+ in if m > 0 andalso n > i' then read i' buf' else Buffer.content buf' end;
+ in read 0 Buffer.empty end;
+
+fun read_line socket =
+ let
+ fun result cs = 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)));
+ (case readN socket 1 of
+ "" => if null cs then NONE else SOME (result cs)
+ | "\n" => SOME (result cs)
+ | c => read (c :: cs));
in read [] end;
+fun write socket =
+ let
+ fun send buf =
+ if Word8VectorSlice.isEmpty buf then ()
+ else
+ let
+ val n = Int.min (Word8VectorSlice.length buf, 4096);
+ val m = Socket.sendVec (socket, Word8VectorSlice.subslice (buf, 0, SOME n));
+ val buf' = Word8VectorSlice.subslice (buf, m, NONE);
+ in send buf' end;
+ in fn s => send (Word8VectorSlice.full (Byte.stringToBytes s)) end;
+
+in
+
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);
+ fun err () = error ("Bad socket name: " ^ quote name);
+ val (host, port) =
+ (case space_explode ":" 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
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}
+ {input_line = fn () => read_line socket,
+ inputN = fn n => readN socket n,
+ output = fn s => write socket s,
+ flush = fn () => ()}
end;
end;
+end;
+
--- a/src/Pure/System/system_channel.scala Fri Sep 23 16:44:51 2011 +0200
+++ b/src/Pure/System/system_channel.scala Fri Sep 23 16:50:39 2011 +0200
@@ -14,7 +14,8 @@
object System_Channel
{
- def apply(): System_Channel = new Fifo_Channel
+ def apply(use_socket: Boolean = false): System_Channel =
+ if (use_socket) new Socket_Channel else new Fifo_Channel
}
abstract class System_Channel
--- a/src/Tools/jEdit/etc/settings Fri Sep 23 16:44:51 2011 +0200
+++ b/src/Tools/jEdit/etc/settings Fri Sep 23 16:50:39 2011 +0200
@@ -10,7 +10,7 @@
JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
-ISABELLE_JEDIT_OPTIONS="-m no_brackets -m no_type_brackets"
+ISABELLE_JEDIT_OPTIONS=""
ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Sep 23 16:44:51 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Sep 23 16:50:39 2011 +0200
@@ -48,6 +48,7 @@
echo " Options are:"
echo " -J OPTION add JVM runtime option"
echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
+ echo " -S BOOL enable socket-based communication (default: named pipe)"
echo " -b build only"
echo " -d enable debugger"
echo " -f fresh build"
@@ -68,6 +69,11 @@
exit 2
}
+function check_bool()
+{
+ [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
+}
+
function failed()
{
fail "Failed!"
@@ -80,18 +86,23 @@
BUILD_ONLY=false
BUILD_JARS="jars"
+JEDIT_USE_SOCKET="false"
JEDIT_LOGIC="$ISABELLE_LOGIC"
JEDIT_PRINT_MODE=""
function getoptions()
{
OPTIND=1
- while getopts "J:bdfj:l:m:" OPT
+ while getopts "J:S: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
;;
@@ -290,7 +301,7 @@
;;
esac
- export JEDIT_LOGIC JEDIT_PRINT_MODE
+ export JEDIT_USE_SOCKET 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 Fri Sep 23 16:44:51 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Fri Sep 23 16:50:39 2011 +0200
@@ -320,13 +320,14 @@
def start_session()
{
val timeout = Time_Property("startup-timeout", Time.seconds(10)) 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, modes ::: List(logic))
+ session.start(timeout, use_socket, modes ::: List(logic))
}