219 } |
219 } |
220 recover(commands) |
220 recover(commands) |
221 } |
221 } |
222 |
222 |
223 |
223 |
224 /* consolidate unfinished spans */ |
|
225 |
|
226 private def consolidate_spans( |
|
227 resources: Resources, |
|
228 syntax: Prover.Syntax, |
|
229 get_blob: Document.Node.Name => Option[Document.Blob], |
|
230 can_import: Document.Node.Name => Boolean, |
|
231 reparse_limit: Int, |
|
232 node_name: Document.Node.Name, |
|
233 header: Document.Node.Header, |
|
234 perspective: Command.Perspective, |
|
235 commands: Linear_Set[Command]): Linear_Set[Command] = |
|
236 { |
|
237 if (perspective.commands.isEmpty) commands |
|
238 else { |
|
239 commands.find(_.is_unfinished) match { |
|
240 case Some(first_unfinished) => |
|
241 val visible = perspective.commands.toSet |
|
242 commands.reverse.find(visible) match { |
|
243 case Some(last_visible) => |
|
244 val it = commands.iterator(last_visible) |
|
245 var last = last_visible |
|
246 var i = 0 |
|
247 while (i < reparse_limit && it.hasNext) { |
|
248 last = it.next |
|
249 i += last.length |
|
250 } |
|
251 reparse_spans(resources, syntax, get_blob, can_import, node_name, |
|
252 header, commands, first_unfinished, last) |
|
253 case None => commands |
|
254 } |
|
255 case None => commands |
|
256 } |
|
257 } |
|
258 } |
|
259 |
|
260 |
|
261 /* main */ |
224 /* main */ |
262 |
225 |
263 def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command]) |
226 def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command]) |
264 : List[Command.Edit] = |
227 : List[Command.Edit] = |
265 { |
228 { |
299 case (name, Document.Node.Perspective(required, text_perspective, overlays)) => |
262 case (name, Document.Node.Perspective(required, text_perspective, overlays)) => |
300 val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays) |
263 val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays) |
301 val perspective: Document.Node.Perspective_Command = |
264 val perspective: Document.Node.Perspective_Command = |
302 Document.Node.Perspective(required, visible_overlay, overlays) |
265 Document.Node.Perspective(required, visible_overlay, overlays) |
303 if (node.same_perspective(text_perspective, perspective)) node |
266 if (node.same_perspective(text_perspective, perspective)) node |
304 else |
267 else { |
305 node.update_perspective(text_perspective, perspective). |
268 /* consolidate unfinished spans */ |
306 update_commands( |
269 val is_visible = visible.commands.toSet |
307 consolidate_spans(resources, syntax, get_blob, can_import, reparse_limit, |
270 val commands = node.commands |
308 name, node.header, visible, node.commands)) |
271 val commands1 = |
|
272 if (is_visible.isEmpty) commands |
|
273 else { |
|
274 commands.find(_.is_unfinished) match { |
|
275 case Some(first_unfinished) => |
|
276 commands.reverse.find(is_visible) match { |
|
277 case Some(last_visible) => |
|
278 val it = commands.iterator(last_visible) |
|
279 var last = last_visible |
|
280 var i = 0 |
|
281 while (i < reparse_limit && it.hasNext) { |
|
282 last = it.next |
|
283 i += last.length |
|
284 } |
|
285 reparse_spans(resources, syntax, get_blob, can_import, name, |
|
286 node.header, commands, first_unfinished, last) |
|
287 case None => commands |
|
288 } |
|
289 case None => commands |
|
290 } |
|
291 } |
|
292 node.update_perspective(text_perspective, perspective).update_commands(commands1) |
|
293 } |
309 } |
294 } |
310 } |
295 } |
311 |
296 |
312 def parse_change( |
297 def parse_change( |
313 resources: Resources, |
298 resources: Resources, |