src/Pure/System/session.scala

   }
 
 
   /* actor messages */
 
-  private case class Start(timeout: Time, use_socket: Boolean, args: List[String])
+  private case class Start(timeout: Time, 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)
   private case class Edit_Node(name: Document.Node.Name,
     header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])

     var finished = false
     while (!finished) {
       receiveWithin(commands_changed_delay.flush_timeout) {
         case TIMEOUT => commands_changed_delay.flush()
 
-        case Start(timeout, use_socket, args) if prover.isEmpty =>
+        case Start(timeout, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
             prover =
-              Some(new Isabelle_Process(timeout, use_socket, receiver.invoke _, args)
-                with Isar_Document)
+              Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isar_Document)
           }
 
         case Stop =>
           if (phase == Session.Ready) {
             global_state.change(_ => Document.State.init)  // FIXME event bus!?

   }
 
 
   /* actions */
 
-  def start(timeout: Time, use_socket: Boolean, args: List[String])
-  { session_actor ! Start(timeout, use_socket, args) }
-
-  def start(args: List[String]) { start (Time.seconds(25), false, args) }
+  def start(timeout: Time, args: List[String])
+  { session_actor ! Start(timeout, args) }
+
+  def start(args: List[String]) { start (Time.seconds(25), args) }
 
   def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
 
   def cancel_execution() { session_actor ! Cancel_Execution }