equal
deleted
inserted
replaced
80 val header: Node_Header, |
80 val header: Node_Header, |
81 val perspective: Command.Perspective, |
81 val perspective: Command.Perspective, |
82 val blobs: Map[String, Blob], |
82 val blobs: Map[String, Blob], |
83 val commands: Linear_Set[Command]) |
83 val commands: Linear_Set[Command]) |
84 { |
84 { |
|
85 def clear: Node = Node.empty.copy(header = header) |
|
86 |
|
87 |
85 /* commands */ |
88 /* commands */ |
86 |
89 |
87 private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = |
90 private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = |
88 { |
91 { |
89 val blocks = new mutable.ListBuffer[(Command, Text.Offset)] |
92 val blocks = new mutable.ListBuffer[(Command, Text.Offset)] |