equal
deleted
inserted
replaced
112 val fitting = children filter(_ fitting_into new_child) |
112 val fitting = children filter(_ fitting_into new_child) |
113 (this remove fitting) add ((new_child /: fitting) (_ + _)) |
113 (this remove fitting) add ((new_child /: fitting) (_ + _)) |
114 } |
114 } |
115 else this set_children new_children |
115 else this set_children new_children |
116 } else { |
116 } else { |
117 error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.info.toString |
117 System.err.println("ignored nonfitting markup: " + new_child) |
118 + "(" +new_child.start + ", "+ new_child.stop + ")") |
118 this |
119 } |
119 } |
120 } |
120 } |
121 |
121 |
122 // does this fit into node? |
122 // does this fit into node? |
123 def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop |
123 def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop |