src/Tools/jEdit/src/document_model.scala
changeset 55435 662e0fd39823
parent 55432 9c53198dbb1c
child 55778 e1fd8780f997
--- a/src/Tools/jEdit/src/document_model.scala	Wed Feb 12 11:05:48 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Feb 12 11:28:17 2014 +0100
@@ -167,7 +167,8 @@
         node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
         node_name -> perspective)
     else
-      List(node_name -> Document.Node.Blob())
+      List(node_name -> Document.Node.Blob(),
+        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))))
   }
 
   def node_edits(
@@ -190,7 +191,8 @@
           node_name -> perspective)
     }
     else
-      List(node_name -> Document.Node.Blob())
+      List(node_name -> Document.Node.Blob(),
+        node_name -> Document.Node.Edits(text_edits))
   }