--- a/src/Tools/jEdit/src/document_model.scala Wed Jul 23 16:20:07 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Jul 23 16:56:03 2014 +0200
@@ -164,22 +164,26 @@
clear: Boolean,
text_edits: List[Text.Edit],
perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
- get_blob() match {
- case None =>
- val header_edit = session.header_edit(node_name, node_header())
- if (clear)
- List(header_edit,
- node_name -> Document.Node.Clear(),
- node_name -> Document.Node.Edits(text_edits),
- node_name -> perspective)
- else
- List(header_edit,
- node_name -> Document.Node.Edits(text_edits),
- node_name -> perspective)
- case Some(blob) =>
- List(node_name -> Document.Node.Blob(blob),
- node_name -> Document.Node.Edits(text_edits))
- }
+ {
+ val edits: List[Document.Edit_Text] =
+ get_blob() match {
+ case None =>
+ val header_edit = session.header_edit(node_name, node_header())
+ if (clear)
+ List(header_edit,
+ node_name -> Document.Node.Clear(),
+ node_name -> Document.Node.Edits(text_edits),
+ node_name -> perspective)
+ else
+ List(header_edit,
+ node_name -> Document.Node.Edits(text_edits),
+ node_name -> perspective)
+ case Some(blob) =>
+ List(node_name -> Document.Node.Blob(blob),
+ node_name -> Document.Node.Edits(text_edits))
+ }
+ edits.filterNot(_._2.is_void)
+ }
/* pending edits */