src/Pure/System/session.scala

     register_document(Document.init)
 
 
     /* document changes */
 
-    def handle_change(change: Change)
+    def handle_change(change: Document.Change)
     //{{{
     {
       require(change.parent.isDefined)
 
       val (node_edits, doc) = change.result.join

           if (prover != null) {
             prover.kill
             prover = null
           }
 
-        case change: Change if prover != null =>
+        case change: Document.Change if prover != null =>
           handle_change(change)
 
         case result: Isabelle_Process.Result =>
           handle_result(result.cache(xml_cache))
 

 
   private case class Edit_Document(edits: List[Document.Node_Text_Edit])
 
   private val editor_history = new Actor
   {
-    @volatile private var history = Change.init
-    def current_change(): Change = history
+    @volatile private var history = Document.Change.init
+    def current_change(): Document.Change = history
 
     def act
     {
       loop {
         react {

               isabelle.Future.fork {
                 val old_doc = old_change.join_document
                 old_doc.await_assignment
                 Document.text_edits(Session.this, old_doc, new_id, edits)
               }
-            val new_change = new Change(new_id, Some(old_change), edits, result)
+            val new_change = new Document.Change(new_id, Some(old_change), edits, result)
             history = new_change
             new_change.result.map(_ => session_actor ! new_change)
 
           case bad => System.err.println("editor_model: ignoring bad message " + bad)
         }

   def started(timeout: Int, args: List[String]): Option[String] =
     (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
 
   def stop() { session_actor ! Stop }
 
-  def current_change(): Change = editor_history.current_change()
+  def current_change(): Document.Change = editor_history.current_change()
   def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history ! Edit_Document(edits) }
 }