changeset 36011 | 3ff725ac13a4 |
parent 34871 | e596a0b71f3c |
child 36012 | 0614676f14d4 |
--- a/src/Pure/Thy/markup_node.scala Mon Mar 29 01:07:01 2010 -0700 +++ b/src/Pure/Thy/markup_node.scala Mon Mar 29 22:43:56 2010 +0200 @@ -70,7 +70,7 @@ markup <- markups } yield markup if (next_x < node.stop) - filled_gaps + new Markup_Node(next_x, node.stop, node.info) + filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info)) else filled_gaps } }