src/Tools/jEdit/src/jedit/document_model.scala
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())
   }