--- 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))
}