--- a/src/Tools/jEdit/src/proofdocument/session.scala Fri Jan 01 14:41:25 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala Fri Jan 01 17:29:35 2010 +0100
@@ -80,9 +80,9 @@
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(""),
@@ -95,8 +95,8 @@
})
}
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)
}
@@ -221,6 +221,7 @@
/* main methods */
+ // FIXME private?
def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
def start(timeout: Int, args: List[String]): Option[String] =