152 } |
152 } |
153 |
153 |
154 final class Commands private(val commands: Linear_Set[Command]) |
154 final class Commands private(val commands: Linear_Set[Command]) |
155 { |
155 { |
156 lazy val thy_load_commands: List[Command] = |
156 lazy val thy_load_commands: List[Command] = |
157 commands.iterator.filter(_.thy_load.isDefined).toList |
157 commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList |
158 |
158 |
159 private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = |
159 private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = |
160 { |
160 { |
161 val blocks = new mutable.ListBuffer[(Command, Text.Offset)] |
161 val blocks = new mutable.ListBuffer[(Command, Text.Offset)] |
162 var next_block = 0 |
162 var next_block = 0 |
187 |
187 |
188 final class Node private( |
188 final class Node private( |
189 val header: Node.Header = Node.bad_header("Bad theory header"), |
189 val header: Node.Header = Node.bad_header("Bad theory header"), |
190 val perspective: Node.Perspective_Command = |
190 val perspective: Node.Perspective_Command = |
191 Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty), |
191 Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty), |
192 val blob: Bytes = Bytes.empty, |
|
193 _commands: Node.Commands = Node.Commands.empty) |
192 _commands: Node.Commands = Node.Commands.empty) |
194 { |
193 { |
195 def clear: Node = new Node(header = header) |
194 def clear: Node = new Node(header = header) |
196 |
195 |
197 def update_header(new_header: Node.Header): Node = |
196 def update_header(new_header: Node.Header): Node = |
198 new Node(new_header, perspective, blob, _commands) |
197 new Node(new_header, perspective, _commands) |
199 |
198 |
200 def update_perspective(new_perspective: Node.Perspective_Command): Node = |
199 def update_perspective(new_perspective: Node.Perspective_Command): Node = |
201 new Node(header, new_perspective, blob, _commands) |
200 new Node(header, new_perspective, _commands) |
202 |
201 |
203 def same_perspective(other_perspective: Node.Perspective_Command): Boolean = |
202 def same_perspective(other_perspective: Node.Perspective_Command): Boolean = |
204 perspective.required == other_perspective.required && |
203 perspective.required == other_perspective.required && |
205 perspective.visible.same(other_perspective.visible) && |
204 perspective.visible.same(other_perspective.visible) && |
206 perspective.overlays == other_perspective.overlays |
205 perspective.overlays == other_perspective.overlays |
207 |
206 |
208 def update_blob(new_blob: Bytes): Node = |
|
209 new Node(header, perspective, new_blob, _commands) |
|
210 |
|
211 def commands: Linear_Set[Command] = _commands.commands |
207 def commands: Linear_Set[Command] = _commands.commands |
212 def thy_load_commands: List[Command] = _commands.thy_load_commands |
208 def thy_load_commands: List[Command] = _commands.thy_load_commands |
213 |
209 |
214 def update_commands(new_commands: Linear_Set[Command]): Node = |
210 def update_commands(new_commands: Linear_Set[Command]): Node = |
215 if (new_commands eq _commands.commands) this |
211 if (new_commands eq _commands.commands) this |
216 else new Node(header, perspective, blob, Node.Commands(new_commands)) |
212 else new Node(header, perspective, Node.Commands(new_commands)) |
217 |
213 |
218 def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = |
214 def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = |
219 _commands.range(i) |
215 _commands.range(i) |
220 |
216 |
221 def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] = |
217 def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] = |