explicit option for socket vs. fifo communication;

--- a/src/Pure/System/isabelle_process.scala	Fri Sep 23 13:43:44 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Fri Sep 23 13:44:31 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 13:43:44 2011 +0200
+++ b/src/Pure/System/session.scala	Fri Sep 23 13:44:31 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.scala	Fri Sep 23 13:43:44 2011 +0200
+++ b/src/Pure/System/system_channel.scala	Fri Sep 23 13:44:31 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/lib/Tools/jedit	Fri Sep 23 13:43:44 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 23 13:44:31 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 13:43:44 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 23 13:44:31 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))
   }