src/Pure/PIDE/session.scala

   case object Shutdown extends Phase  // transient
   //}}}
 
 
   /* protocol handlers */
-
-  type Prover = Isabelle_Process with Protocol
 
   abstract class Protocol_Handler
   {
     def stop(prover: Prover): Unit = {}
     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]

   }
 
 
   /* actor messages */
 
-  private case class Start(args: List[String])
+  private case class Start(name: String, args: List[String])
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
   private case class Messages(msgs: List[Prover.Message])
   private case class Update_Options(options: Options)
 

       timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
 
       def cancel() { timer.cancel() }
     }
 
-    var prover: Option[Session.Prover] = None
+    var prover: Option[Prover] = None
 
 
     /* delayed command changes */
 
     object delay_commands_changed

     var finished = false
     while (!finished) {
       receiveWithin(delay_commands_changed.flush_timeout) {
         case TIMEOUT => delay_commands_changed.flush()
 
-        case Start(args) if prover.isEmpty =>
+        case Start(name, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
-            prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
+            prover = Some(resources.start_prover(receiver.invoke _, name, args))
           }
 
         case Stop =>
           if (phase == Session.Ready) {
             _protocol_handlers = _protocol_handlers.stop(prover.get)

   }
 
 
   /* actions */
 
-  def start(args: List[String])
-  {
-    session_actor ! Start(args)
+  def start(name: String, args: List[String])
+  {
+    session_actor ! Start(name, args)
   }
 
   def stop()
   {
     commands_changed_buffer !? Stop