src/Pure/PIDE/markup.scala
changeset 56743 81370dfadb1d
parent 56733 f7700146678d
child 56843 b2bfcd8cda80
     1.1 --- a/src/Pure/PIDE/markup.scala	Sat Apr 26 06:43:06 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat Apr 26 13:07:20 2014 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Module:     PIDE
     1.5      Author:     Makarius
     1.6  
     1.7 -Isabelle-specific implementation of quasi-abstract markup elements.
     1.8 +Quasi-abstract markup elements.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -10,6 +10,30 @@
    1.13  
    1.14  object Markup
    1.15  {
    1.16 +  /* elements */
    1.17 +
    1.18 +  object Elements
    1.19 +  {
    1.20 +    def apply(elems: Set[String]): Elements = new Elements(elems)
    1.21 +    def apply(elems: String*): Elements = apply(Set(elems: _*))
    1.22 +    val empty: Elements = apply()
    1.23 +    val full: Elements =
    1.24 +      new Elements(Set.empty)
    1.25 +      {
    1.26 +        override def apply(elem: String): Boolean = true
    1.27 +        override def toString: String = "Elements.full"
    1.28 +      }
    1.29 +  }
    1.30 +
    1.31 +  sealed class Elements private[Markup](private val rep: Set[String])
    1.32 +  {
    1.33 +    def apply(elem: String): Boolean = rep.contains(elem)
    1.34 +    def + (elem: String): Elements = new Elements(rep + elem)
    1.35 +    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
    1.36 +    override def toString: String = rep.mkString("Elements(", ",", ")")
    1.37 +  }
    1.38 +
    1.39 +
    1.40    /* properties */
    1.41  
    1.42    val NAME = "name"