1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 10 16:40:21 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 10 17:10:32 2010 +0100
     1.3 @@ -64,14 +64,7 @@
     1.4      new Change(document_0.id, None, Nil, Future.value(Nil, document_0))
     1.5  
     1.6    def current_change(): Change = history
     1.7 -
     1.8 -  def recent_document(): Document =
     1.9 -  {
    1.10 -    def find(change: Change): Change =
    1.11 -      if (change.result.is_finished && change.join_document.assignment.is_finished) change
    1.12 -      else find(change.parent.get)
    1.13 -    find(current_change()).join_document
    1.14 -  }
    1.15 +  def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
    1.16  
    1.17  
    1.18    /* transforming offsets */

     2.1 --- a/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 10 16:40:21 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 10 17:10:32 2010 +0100
     2.3 @@ -26,6 +26,7 @@
     2.4    }
     2.5  
     2.6    def join_document: Document = result.join._2
     2.7 +  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
     2.8  
     2.9    def edit(session: Session, edits: List[Text_Edit]): Change =
    2.10    {