src/Pure/System/session.scala

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

           catch {
             case _: Document.State.Fail => bad_result(result)
           }
         case Isabelle_Markup.Assign_Execs if result.is_raw =>
           XML.content(result.body).mkString match {
-            case Isabelle_Document.Assign(id, assign) =>
+            case Protocol.Assign(id, assign) =>
               try { handle_assign(id, assign) }
               catch { case _: Document.State.Fail => bad_result(result) }
             case _ => bad_result(result)
           }
           // FIXME separate timeout event/message!?

             if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
             prune_next = System.currentTimeMillis() + prune_delay.ms
           }
         case Isabelle_Markup.Removed_Versions if result.is_raw =>
           XML.content(result.body).mkString match {
-            case Isabelle_Document.Removed(removed) =>
+            case Protocol.Removed(removed) =>
               try { handle_removed(removed) }
               catch { case _: Document.State.Fail => bad_result(result) }
             case _ => bad_result(result)
           }
         case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>

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