src/Pure/PIDE/markup.scala
changeset 65176 908d8be90533
parent 64370 865b39487b5d
child 65313 347ed6219dab
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri Mar 10 18:12:52 2017 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Fri Mar 10 21:47:48 2017 +0100
     1.3 @@ -29,6 +29,8 @@
     1.4      def apply(elem: String): Boolean = rep.contains(elem)
     1.5      def + (elem: String): Elements = new Elements(rep + elem)
     1.6      def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
     1.7 +    def - (elem: String): Elements = new Elements(rep - elem)
     1.8 +    def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
     1.9      override def toString: String = rep.mkString("Elements(", ",", ")")
    1.10    }
    1.11