162 |
162 |
163 def node_edits( |
163 def node_edits( |
164 clear: Boolean, |
164 clear: Boolean, |
165 text_edits: List[Text.Edit], |
165 text_edits: List[Text.Edit], |
166 perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] = |
166 perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] = |
167 get_blob() match { |
167 { |
168 case None => |
168 val edits: List[Document.Edit_Text] = |
169 val header_edit = session.header_edit(node_name, node_header()) |
169 get_blob() match { |
170 if (clear) |
170 case None => |
171 List(header_edit, |
171 val header_edit = session.header_edit(node_name, node_header()) |
172 node_name -> Document.Node.Clear(), |
172 if (clear) |
173 node_name -> Document.Node.Edits(text_edits), |
173 List(header_edit, |
174 node_name -> perspective) |
174 node_name -> Document.Node.Clear(), |
175 else |
175 node_name -> Document.Node.Edits(text_edits), |
176 List(header_edit, |
176 node_name -> perspective) |
177 node_name -> Document.Node.Edits(text_edits), |
177 else |
178 node_name -> perspective) |
178 List(header_edit, |
179 case Some(blob) => |
179 node_name -> Document.Node.Edits(text_edits), |
180 List(node_name -> Document.Node.Blob(blob), |
180 node_name -> perspective) |
181 node_name -> Document.Node.Edits(text_edits)) |
181 case Some(blob) => |
182 } |
182 List(node_name -> Document.Node.Blob(blob), |
|
183 node_name -> Document.Node.Edits(text_edits)) |
|
184 } |
|
185 edits.filterNot(_._2.is_void) |
|
186 } |
183 |
187 |
184 |
188 |
185 /* pending edits */ |
189 /* pending edits */ |
186 |
190 |
187 private object pending_edits // owned by GUI thread |
191 private object pending_edits // owned by GUI thread |