--- a/src/Pure/PIDE/markup.scala Fri Mar 10 18:12:52 2017 +0100
+++ b/src/Pure/PIDE/markup.scala Fri Mar 10 21:47:48 2017 +0100
@@ -29,6 +29,8 @@
def apply(elem: String): Boolean = rep.contains(elem)
def + (elem: String): Elements = new Elements(rep + elem)
def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
+ def - (elem: String): Elements = new Elements(rep - elem)
+ def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
override def toString: String = rep.mkString("Elements(", ",", ")")
}