src/Pure/PIDE/markup_tree.scala

--- 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(", ",", ")")
     }
 }
-