90 |
90 |
91 |
91 |
92 |
92 |
93 /** perspective **/ |
93 /** perspective **/ |
94 |
94 |
95 def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective = |
95 def command_perspective( |
96 { |
96 node: Document.Node, |
97 if (perspective.is_empty) Command.Perspective.empty |
97 perspective: Text.Perspective, |
|
98 overlays: Document.Overlays): (Command.Perspective, Command.Perspective) = |
|
99 { |
|
100 if (perspective.is_empty && overlays.is_empty) |
|
101 (Command.Perspective.empty, Command.Perspective.empty) |
98 else { |
102 else { |
99 val result = new mutable.ListBuffer[Command] |
103 val has_overlay = overlays.commands |
|
104 val visible = new mutable.ListBuffer[Command] |
|
105 val visible_overlay = new mutable.ListBuffer[Command] |
100 @tailrec |
106 @tailrec |
101 def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)]) |
107 def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)]) |
102 { |
108 { |
103 (ranges, commands) match { |
109 (ranges, commands) match { |
104 case (range :: more_ranges, (command, offset) #:: more_commands) => |
110 case (range :: more_ranges, (command, offset) #:: more_commands) => |
105 val command_range = command.range + offset |
111 val command_range = command.range + offset |
106 range compare command_range match { |
112 range compare command_range match { |
107 case -1 => check_ranges(more_ranges, commands) |
|
108 case 0 => |
113 case 0 => |
109 result += command |
114 visible += command |
|
115 visible_overlay += command |
110 check_ranges(ranges, more_commands) |
116 check_ranges(ranges, more_commands) |
111 case 1 => check_ranges(ranges, more_commands) |
117 case c => |
|
118 if (has_overlay(command)) visible_overlay += command |
|
119 |
|
120 if (c < 0) check_ranges(more_ranges, commands) |
|
121 else check_ranges(ranges, more_commands) |
112 } |
122 } |
|
123 |
|
124 case (Nil, (command, _) #:: more_commands) => |
|
125 if (has_overlay(command)) visible_overlay += command |
|
126 |
|
127 check_ranges(Nil, more_commands) |
|
128 |
113 case _ => |
129 case _ => |
114 } |
130 } |
115 } |
131 } |
116 check_ranges(perspective.ranges, node.command_range(perspective.range).toStream) |
132 |
117 Command.Perspective(result.toList) |
133 val commands = |
|
134 if (overlays.is_empty) node.command_range(perspective.range) |
|
135 else node.command_range() |
|
136 check_ranges(perspective.ranges, commands.toStream) |
|
137 (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList)) |
118 } |
138 } |
119 } |
139 } |
120 |
140 |
121 |
141 |
122 |
142 |
315 node.update_commands(commands2) |
335 node.update_commands(commands2) |
316 |
336 |
317 case (_, Document.Node.Deps(_)) => node |
337 case (_, Document.Node.Deps(_)) => node |
318 |
338 |
319 case (name, Document.Node.Perspective(required, text_perspective, overlays)) => |
339 case (name, Document.Node.Perspective(required, text_perspective, overlays)) => |
|
340 val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays) |
320 val perspective: Document.Node.Perspective_Command = |
341 val perspective: Document.Node.Perspective_Command = |
321 Document.Node.Perspective(required, command_perspective(node, text_perspective), overlays) |
342 Document.Node.Perspective(required, visible_overlay, overlays) |
322 if (node.same_perspective(perspective)) node |
343 if (node.same_perspective(perspective)) node |
323 else |
344 else |
324 node.update_perspective(perspective).update_commands( |
345 node.update_perspective(perspective).update_commands( |
325 consolidate_spans(syntax, reparse_limit, name, perspective.visible, node.commands)) |
346 consolidate_spans(syntax, reparse_limit, name, visible, node.commands)) |
326 } |
347 } |
327 } |
348 } |
328 |
349 |
329 def text_edits( |
350 def text_edits( |
330 base_syntax: Outer_Syntax, |
351 base_syntax: Outer_Syntax, |