explicit option for socket vs. fifo communication;
authorwenzelm
Fri Sep 23 13:44:31 2011 +0200 (2011-09-23)
changeset 4505555274f7e306b
parent 45054 73accf69135d
child 45056 bbd7eac14df3
explicit option for socket vs. fifo communication;
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Pure/System/system_channel.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/System/isabelle_process.scala	Fri Sep 23 13:43:44 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Fri Sep 23 13:44:31 2011 +0200
     1.3 @@ -75,16 +75,15 @@
     1.4  }
     1.5  
     1.6  
     1.7 -class Isabelle_Process(timeout: Time, receiver: Isabelle_Process.Message => Unit, args: String*)
     1.8 +class Isabelle_Process(
     1.9 +    timeout: Time = Time.seconds(10),
    1.10 +    use_socket: Boolean = false,
    1.11 +    receiver: Isabelle_Process.Message => Unit = Console.println(_),
    1.12 +    args: List[String] = Nil)
    1.13  {
    1.14    import Isabelle_Process._
    1.15  
    1.16  
    1.17 -  /* demo constructor */
    1.18 -
    1.19 -  def this(args: String*) = this(Time.seconds(10), Console.println(_), args: _*)
    1.20 -
    1.21 -
    1.22    /* results */
    1.23  
    1.24    private def system_result(text: String)
    1.25 @@ -131,13 +130,13 @@
    1.26  
    1.27    /** process manager **/
    1.28  
    1.29 -  private val system_channel = System_Channel()
    1.30 +  private val system_channel = System_Channel(use_socket)
    1.31  
    1.32    private val process =
    1.33      try {
    1.34        val cmdline =
    1.35          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
    1.36 -          (system_channel.isabelle_args ::: args.toList)
    1.37 +          (system_channel.isabelle_args ::: args)
    1.38        new Isabelle_System.Managed_Process(true, cmdline: _*)
    1.39      }
    1.40      catch { case e: IOException => system_channel.accepted(); throw(e) }
     2.1 --- a/src/Pure/System/session.scala	Fri Sep 23 13:43:44 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Fri Sep 23 13:44:31 2011 +0200
     2.3 @@ -137,7 +137,7 @@
     2.4  
     2.5    /* actor messages */
     2.6  
     2.7 -  private case class Start(timeout: Time, args: List[String])
     2.8 +  private case class Start(timeout: Time, use_socket: Boolean, args: List[String])
     2.9    private case object Cancel_Execution
    2.10    private case class Init_Node(name: Document.Node.Name,
    2.11      header: Document.Node_Header, perspective: Text.Perspective, text: String)
    2.12 @@ -405,11 +405,12 @@
    2.13        receiveWithin(commands_changed_delay.flush_timeout) {
    2.14          case TIMEOUT => commands_changed_delay.flush()
    2.15  
    2.16 -        case Start(timeout, args) if prover.isEmpty =>
    2.17 +        case Start(timeout, use_socket, args) if prover.isEmpty =>
    2.18            if (phase == Session.Inactive || phase == Session.Failed) {
    2.19              phase = Session.Startup
    2.20              prover =
    2.21 -              Some(new Isabelle_Process(timeout, receiver.invoke _, args:_*) with Isar_Document)
    2.22 +              Some(new Isabelle_Process(timeout, use_socket, receiver.invoke _, args)
    2.23 +                with Isar_Document)
    2.24            }
    2.25  
    2.26          case Stop =>
    2.27 @@ -468,7 +469,8 @@
    2.28  
    2.29    /* actions */
    2.30  
    2.31 -  def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
    2.32 +  def start(timeout: Time = Time.seconds(10), use_socket: Boolean = false, args: List[String])
    2.33 +  { session_actor ! Start(timeout, use_socket, args) }
    2.34  
    2.35    def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
    2.36  
     3.1 --- a/src/Pure/System/system_channel.scala	Fri Sep 23 13:43:44 2011 +0200
     3.2 +++ b/src/Pure/System/system_channel.scala	Fri Sep 23 13:44:31 2011 +0200
     3.3 @@ -14,7 +14,8 @@
     3.4  
     3.5  object System_Channel
     3.6  {
     3.7 -  def apply(): System_Channel = new Fifo_Channel
     3.8 +  def apply(use_socket: Boolean = false): System_Channel =
     3.9 +    if (use_socket) new Socket_Channel else new Fifo_Channel
    3.10  }
    3.11  
    3.12  abstract class System_Channel
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 23 13:43:44 2011 +0200
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 23 13:44:31 2011 +0200
     4.3 @@ -48,6 +48,7 @@
     4.4    echo "  Options are:"
     4.5    echo "    -J OPTION    add JVM runtime option"
     4.6    echo "                 (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
     4.7 +  echo "    -S BOOL      enable socket-based communication (default: named pipe)"
     4.8    echo "    -b           build only"
     4.9    echo "    -d           enable debugger"
    4.10    echo "    -f           fresh build"
    4.11 @@ -68,6 +69,11 @@
    4.12    exit 2
    4.13  }
    4.14  
    4.15 +function check_bool()
    4.16 +{
    4.17 +  [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
    4.18 +}
    4.19 +
    4.20  function failed()
    4.21  {
    4.22    fail "Failed!"
    4.23 @@ -80,18 +86,23 @@
    4.24  
    4.25  BUILD_ONLY=false
    4.26  BUILD_JARS="jars"
    4.27 +JEDIT_USE_SOCKET="false"
    4.28  JEDIT_LOGIC="$ISABELLE_LOGIC"
    4.29  JEDIT_PRINT_MODE=""
    4.30  
    4.31  function getoptions()
    4.32  {
    4.33    OPTIND=1
    4.34 -  while getopts "J:bdfj:l:m:" OPT
    4.35 +  while getopts "J:S:bdfj:l:m:" OPT
    4.36    do
    4.37      case "$OPT" in
    4.38        J)
    4.39          JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
    4.40          ;;
    4.41 +      S)
    4.42 +        check_bool "$OPTARG"
    4.43 +        JEDIT_USE_SOCKET="$OPTARG"
    4.44 +        ;;
    4.45        b)
    4.46          BUILD_ONLY=true
    4.47          ;;
    4.48 @@ -290,7 +301,7 @@
    4.49        ;;
    4.50    esac
    4.51  
    4.52 -  export JEDIT_LOGIC JEDIT_PRINT_MODE
    4.53 +  export JEDIT_USE_SOCKET JEDIT_LOGIC JEDIT_PRINT_MODE
    4.54  
    4.55    exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
    4.56      -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Sep 23 13:43:44 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 23 13:44:31 2011 +0200
     5.3 @@ -320,13 +320,14 @@
     5.4    def start_session()
     5.5    {
     5.6      val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
     5.7 +    val use_socket = Isabelle_System.getenv("JEDIT_USE_SOCKET") == "true"
     5.8      val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     5.9      val logic = {
    5.10        val logic = Property("logic")
    5.11        if (logic != null && logic != "") logic
    5.12        else Isabelle.default_logic()
    5.13      }
    5.14 -    session.start(timeout, modes ::: List(logic))
    5.15 +    session.start(timeout, use_socket, modes ::: List(logic))
    5.16    }
    5.17  
    5.18