# HG changeset patch
# User wenzelm
# Date 1263139832 -3600
# Node ID 64c2eb92df9f2649be2063f5d98a1d1b0a6b9a8c
# Parent  32b49207ca207730246d3be00d84c6ff16ce01a5
tuned document changes;

diff -r 32b49207ca20 -r 64c2eb92df9f src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 10 16:40:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 10 17:10:32 2010 +0100
@@ -64,14 +64,7 @@
     new Change(document_0.id, None, Nil, Future.value(Nil, document_0))
 
   def current_change(): Change = history
-
-  def recent_document(): Document =
-  {
-    def find(change: Change): Change =
-      if (change.result.is_finished && change.join_document.assignment.is_finished) change
-      else find(change.parent.get)
-    find(current_change()).join_document
-  }
+  def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
 
 
   /* transforming offsets */
diff -r 32b49207ca20 -r 64c2eb92df9f src/Tools/jEdit/src/proofdocument/change.scala
--- a/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 10 16:40:21 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 10 17:10:32 2010 +0100
@@ -26,6 +26,7 @@
   }
 
   def join_document: Document = result.join._2
+  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
 
   def edit(session: Session, edits: List[Text_Edit]): Change =
   {