99 |
99 |
100 /** perspective **/ |
100 /** perspective **/ |
101 |
101 |
102 def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective = |
102 def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective = |
103 { |
103 { |
104 if (perspective.is_empty) Nil |
104 if (perspective.is_empty) Command.Perspective.empty |
105 else { |
105 else { |
106 val result = new mutable.ListBuffer[Command] |
106 val result = new mutable.ListBuffer[Command] |
107 @tailrec |
107 @tailrec |
108 def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)]) |
108 def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)]) |
109 { |
109 { |
119 } |
119 } |
120 case _ => |
120 case _ => |
121 } |
121 } |
122 } |
122 } |
123 check_ranges(perspective.ranges, node.command_range(perspective.range).toStream) |
123 check_ranges(perspective.ranges, node.command_range(perspective.range).toStream) |
124 result.toList |
124 Command.Perspective(result.toList) |
125 } |
125 } |
126 } |
126 } |
127 |
127 |
128 def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective) |
128 def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective) |
129 : (Command.Perspective, Option[Document.Nodes]) = |
129 : (Command.Perspective, Option[Document.Nodes]) = |
130 { |
130 { |
131 val node = nodes(name) |
131 val node = nodes(name) |
132 val perspective = command_perspective(node, text_perspective) |
132 val perspective = command_perspective(node, text_perspective) |
133 val new_nodes = |
133 val new_nodes = |
134 if (Command.equal_perspective(node.perspective, perspective)) None |
134 if (node.perspective same perspective) None |
135 else Some(nodes + (name -> node.copy(perspective = perspective))) |
135 else Some(nodes + (name -> node.copy(perspective = perspective))) |
136 (perspective, new_nodes) |
136 (perspective, new_nodes) |
137 } |
137 } |
138 |
138 |
139 def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective) |
139 def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective) |