17 def command_perspective( |
17 def command_perspective( |
18 node: Document.Node, |
18 node: Document.Node, |
19 perspective: Text.Perspective, |
19 perspective: Text.Perspective, |
20 overlays: Document.Node.Overlays |
20 overlays: Document.Node.Overlays |
21 ): (Command.Perspective, Command.Perspective) = { |
21 ): (Command.Perspective, Command.Perspective) = { |
22 if (perspective.is_empty && overlays.is_empty) |
22 if (perspective.is_empty && overlays.is_empty) { |
23 (Command.Perspective.empty, Command.Perspective.empty) |
23 (Command.Perspective.empty, Command.Perspective.empty) |
|
24 } |
24 else { |
25 else { |
25 val has_overlay = overlays.commands |
26 val has_overlay = overlays.commands |
26 val visible = new mutable.ListBuffer[Command] |
27 val visible = new mutable.ListBuffer[Command] |
27 val visible_overlay = new mutable.ListBuffer[Command] |
28 val visible_overlay = new mutable.ListBuffer[Command] |
28 @tailrec def check_ranges( |
29 @tailrec def check_ranges( |
213 resources: Resources, |
214 resources: Resources, |
214 syntax: Outer_Syntax, |
215 syntax: Outer_Syntax, |
215 get_blob: Document.Node.Name => Option[Document.Blob], |
216 get_blob: Document.Node.Name => Option[Document.Blob], |
216 can_import: Document.Node.Name => Boolean, |
217 can_import: Document.Node.Name => Boolean, |
217 reparse_limit: Int, |
218 reparse_limit: Int, |
218 node: Document.Node, edit: Document.Edit_Text |
219 node: Document.Node, |
|
220 edit: Document.Edit_Text |
219 ): Document.Node = { |
221 ): Document.Node = { |
220 /* recover command spans after edits */ |
222 /* recover command spans after edits */ |
221 // FIXME somewhat slow |
223 // FIXME somewhat slow |
222 def recover_spans( |
224 def recover_spans( |
223 name: Document.Node.Name, |
225 name: Document.Node.Name, |
311 if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes)) |
313 if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes)) |
312 else { |
314 else { |
313 val reparse = |
315 val reparse = |
314 nodes0.iterator.foldLeft(syntax_changed) { |
316 nodes0.iterator.foldLeft(syntax_changed) { |
315 case (reparse, (name, node)) => |
317 case (reparse, (name, node)) => |
316 if (node.load_commands_changed(doc_blobs) && !reparse.contains(name)) |
318 if (node.load_commands_changed(doc_blobs) && !reparse.contains(name)) { |
317 name :: reparse |
319 name :: reparse |
|
320 } |
318 else reparse |
321 else reparse |
319 } |
322 } |
320 val reparse_set = reparse.toSet |
323 val reparse_set = reparse.toSet |
321 |
324 |
322 var nodes = nodes0 |
325 var nodes = nodes0 |
331 val node = nodes(name) |
334 val node = nodes(name) |
332 val syntax = resources.session_base.node_syntax(nodes, name) |
335 val syntax = resources.session_base.node_syntax(nodes, name) |
333 val commands = node.commands |
336 val commands = node.commands |
334 |
337 |
335 val node1 = |
338 val node1 = |
336 if (reparse_set(name) && commands.nonEmpty) |
339 if (reparse_set(name) && commands.nonEmpty) { |
337 node.update_commands( |
340 node.update_commands( |
338 reparse_spans(resources, syntax, get_blob, can_import, name, |
341 reparse_spans(resources, syntax, get_blob, can_import, name, |
339 commands, commands.head, commands.last)) |
342 commands, commands.head, commands.last)) |
|
343 } |
340 else node |
344 else node |
341 val node2 = |
345 val node2 = |
342 edits.foldLeft(node1)( |
346 edits.foldLeft(node1)( |
343 text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _)) |
347 text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _)) |
344 val node3 = |
348 val node3 = |
345 if (reparse_set.contains(name)) |
349 if (reparse_set.contains(name)) { |
346 text_edit(resources, syntax, get_blob, can_import, reparse_limit, |
350 text_edit(resources, syntax, get_blob, can_import, reparse_limit, |
347 node2, (name, node2.edit_perspective)) |
351 node2, (name, node2.edit_perspective)) |
|
352 } |
348 else node2 |
353 else node2 |
349 |
354 |
350 if (!node.same_perspective(node3.text_perspective, node3.perspective)) |
355 if (!node.same_perspective(node3.text_perspective, node3.perspective)) { |
351 doc_edits += (name -> node3.perspective) |
356 doc_edits += (name -> node3.perspective) |
|
357 } |
352 |
358 |
353 doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands))) |
359 doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands))) |
354 |
360 |
355 nodes += (name -> node3) |
361 nodes += (name -> node3) |
356 } |
362 } |