changeset 36011 | 3ff725ac13a4 |
parent 34871 | e596a0b71f3c |
child 36012 | 0614676f14d4 |
36010:a5e7574d8214 | 36011:3ff725ac13a4 |
---|---|
68 else child.flatten |
68 else child.flatten |
69 update = (next_x = child.node.stop) |
69 update = (next_x = child.node.stop) |
70 markup <- markups |
70 markup <- markups |
71 } yield markup |
71 } yield markup |
72 if (next_x < node.stop) |
72 if (next_x < node.stop) |
73 filled_gaps + new Markup_Node(next_x, node.stop, node.info) |
73 filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info)) |
74 else filled_gaps |
74 else filled_gaps |
75 } |
75 } |
76 } |
76 } |
77 } |
77 } |
78 |
78 |