changeset 34835 | 67733fd0e3fa |
parent 34834 | df9af932e418 |
child 34838 | 08a72dc4868e |
--- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 04 00:13:09 2010 +0100 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 04 19:08:10 2010 +0100 @@ -68,7 +68,8 @@ def recent_document(): Document = { def find(change: Change): Document = - if (change.result.is_finished || !change.parent.isDefined) change.document + if (change.result.is_finished && change.document.is_assigned || !change.parent.isDefined) + change.document else find(change.parent.get) find(current_change()) }