119 } |
123 } |
120 case class Clear[A, B]() extends Edit[A, B] |
124 case class Clear[A, B]() extends Edit[A, B] |
121 case class Edits[A, B](edits: List[A]) extends Edit[A, B] |
125 case class Edits[A, B](edits: List[A]) extends Edit[A, B] |
122 case class Deps[A, B](header: Header) extends Edit[A, B] |
126 case class Deps[A, B](header: Header) extends Edit[A, B] |
123 case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B] |
127 case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B] |
|
128 case class Blob[A, B](blob: Bytes) extends Edit[A, B] |
124 type Perspective_Text = Perspective[Text.Edit, Text.Perspective] |
129 type Perspective_Text = Perspective[Text.Edit, Text.Perspective] |
125 type Perspective_Command = Perspective[Command.Edit, Command.Perspective] |
130 type Perspective_Command = Perspective[Command.Edit, Command.Perspective] |
126 |
131 |
127 |
132 |
128 /* commands */ |
133 /* commands */ |
182 |
187 |
183 final class Node private( |
188 final class Node private( |
184 val header: Node.Header = Node.bad_header("Bad theory header"), |
189 val header: Node.Header = Node.bad_header("Bad theory header"), |
185 val perspective: Node.Perspective_Command = |
190 val perspective: Node.Perspective_Command = |
186 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, |
187 _commands: Node.Commands = Node.Commands.empty) |
193 _commands: Node.Commands = Node.Commands.empty) |
188 { |
194 { |
189 def clear: Node = new Node(header = header) |
195 def clear: Node = new Node(header = header) |
190 |
196 |
191 def update_header(new_header: Node.Header): Node = |
197 def update_header(new_header: Node.Header): Node = |
192 new Node(new_header, perspective, _commands) |
198 new Node(new_header, perspective, blob, _commands) |
193 |
199 |
194 def update_perspective(new_perspective: Node.Perspective_Command): Node = |
200 def update_perspective(new_perspective: Node.Perspective_Command): Node = |
195 new Node(header, new_perspective, _commands) |
201 new Node(header, new_perspective, blob, _commands) |
196 |
202 |
197 def same_perspective(other_perspective: Node.Perspective_Command): Boolean = |
203 def same_perspective(other_perspective: Node.Perspective_Command): Boolean = |
198 perspective.required == other_perspective.required && |
204 perspective.required == other_perspective.required && |
199 perspective.visible.same(other_perspective.visible) && |
205 perspective.visible.same(other_perspective.visible) && |
200 perspective.overlays == other_perspective.overlays |
206 perspective.overlays == other_perspective.overlays |
201 |
207 |
|
208 def update_blob(new_blob: Bytes): Node = |
|
209 new Node(header, perspective, new_blob, _commands) |
|
210 |
202 def commands: Linear_Set[Command] = _commands.commands |
211 def commands: Linear_Set[Command] = _commands.commands |
203 def thy_load_commands: List[Command] = _commands.thy_load_commands |
212 def thy_load_commands: List[Command] = _commands.thy_load_commands |
204 |
213 |
205 def update_commands(new_commands: Linear_Set[Command]): Node = |
214 def update_commands(new_commands: Linear_Set[Command]): Node = |
206 if (new_commands eq _commands.commands) this |
215 if (new_commands eq _commands.commands) this |
207 else new Node(header, perspective, Node.Commands(new_commands)) |
216 else new Node(header, perspective, blob, Node.Commands(new_commands)) |
208 |
217 |
209 def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = |
218 def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = |
210 _commands.range(i) |
219 _commands.range(i) |
211 |
220 |
212 def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] = |
221 def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] = |