changeset 60215 | 5fb4990dfc73 |
parent 58463 | 0bf0e9788d54 |
child 64370 | 865b39487b5d |
--- a/src/Pure/PIDE/markup_tree.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Sun May 03 00:01:10 2015 +0200 @@ -57,7 +57,7 @@ def filter_markup(elements: Markup.Elements): List[XML.Elem] = { var result: List[XML.Elem] = Nil - for { elem <- rev_markup; if (elements(elem.name)) } + for (elem <- rev_markup if elements(elem.name)) result ::= elem result.toList } @@ -267,4 +267,3 @@ case list => list.mkString("Tree(", ",", ")") } } -