src/Tools/jEdit/src/proofdocument/session.scala

 
     /* document changes */
 
     def handle_change(change: Change)
     {
-      val old = document(change.parent.get.id).get
-      val (doc, changes) = old.text_changed(this, change)
-
+      require(change.parent.isDefined)
+
+      val (doc, changes) = change.result()  // FIXME clarify future vs. actor arrangement
       val id_changes = changes map {
         case (c1, c2) =>
           (c1.map(_.id).getOrElse(""),
            c2 match {
               case None => None

                 prover.define_command(command.id, system.symbols.encode(command.content))
                 Some(command.id)
             })
       }
       register(doc)
-      documents += (doc.id -> doc)
-      prover.edit_document(old.id, doc.id, id_changes)
+      documents += (doc.id -> doc)  // FIXME remove
+      prover.edit_document(change.parent.get.document.id, doc.id, id_changes)
 
       document_change.event(doc)
     }
 
 

   }
 
 
   /* main methods */
 
+  // FIXME private?
   def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
 
   def start(timeout: Int, args: List[String]): Option[String] =
     (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]