# HG changeset patch
# User wenzelm
# Date 1316789439 -7200
# Node ID b099f5cfd32c15824d6f09ab48724d440cd0c64e
# Parent  b3b50d8b535a81be1ef268437059be8eaf65fd1d# Parent  8b20be429cf33116fe4168cb36b3b5495c3ad9f9
merged;

diff -r b3b50d8b535a -r b099f5cfd32c bin/isabelle-process
--- 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 ();"
 
diff -r b3b50d8b535a -r b099f5cfd32c src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- 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]:
diff -r b3b50d8b535a -r b099f5cfd32c src/Pure/Syntax/syntax_trans.ML
--- 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)
diff -r b3b50d8b535a -r b099f5cfd32c src/Pure/System/isabelle_process.ML
--- 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;
diff -r b3b50d8b535a -r b099f5cfd32c src/Pure/System/isabelle_process.scala
--- 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) }
diff -r b3b50d8b535a -r b099f5cfd32c src/Pure/System/session.scala
--- 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 }
 
diff -r b3b50d8b535a -r b099f5cfd32c src/Pure/System/system_channel.ML
--- 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;
+
diff -r b3b50d8b535a -r b099f5cfd32c src/Pure/System/system_channel.scala
--- 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
diff -r b3b50d8b535a -r b099f5cfd32c src/Tools/jEdit/etc/settings
--- 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"
 
diff -r b3b50d8b535a -r b099f5cfd32c src/Tools/jEdit/lib/Tools/jedit
--- 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")" \
diff -r b3b50d8b535a -r b099f5cfd32c src/Tools/jEdit/src/plugin.scala
--- 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))
   }