src/Pure/PIDE/document.scala
changeset 56743 81370dfadb1d
parent 56711 ef3d00153e3b
child 56746 d37a5d09a277
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Apr 26 06:43:06 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Apr 26 13:07:20 2014 +0200
     1.3 @@ -379,31 +379,6 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* markup elements */
     1.8 -
     1.9 -  object Elements
    1.10 -  {
    1.11 -    def apply(elems: Set[String]): Elements = new Elements(elems)
    1.12 -    def apply(elems: String*): Elements = apply(Set(elems: _*))
    1.13 -    val empty: Elements = apply()
    1.14 -    val full: Elements = new Full_Elements
    1.15 -  }
    1.16 -
    1.17 -  sealed class Elements private[Document](private val rep: Set[String])
    1.18 -  {
    1.19 -    def apply(elem: String): Boolean = rep.contains(elem)
    1.20 -    def + (elem: String): Elements = new Elements(rep + elem)
    1.21 -    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
    1.22 -    override def toString: String = rep.mkString("Elements(", ",", ")")
    1.23 -  }
    1.24 -
    1.25 -  private class Full_Elements extends Elements(Set.empty)
    1.26 -  {
    1.27 -    override def apply(elem: String): Boolean = true
    1.28 -    override def toString: String = "Full_Elements()"
    1.29 -  }
    1.30 -
    1.31 -
    1.32    /* snapshot */
    1.33  
    1.34    object Snapshot
    1.35 @@ -431,13 +406,13 @@
    1.36      def cumulate[A](
    1.37        range: Text.Range,
    1.38        info: A,
    1.39 -      elements: Elements,
    1.40 +      elements: Markup.Elements,
    1.41        result: List[Command.State] => (A, Text.Markup) => Option[A],
    1.42        status: Boolean = false): List[Text.Info[A]]
    1.43  
    1.44      def select[A](
    1.45        range: Text.Range,
    1.46 -      elements: Elements,
    1.47 +      elements: Markup.Elements,
    1.48        result: List[Command.State] => Text.Markup => Option[A],
    1.49        status: Boolean = false): List[Text.Info[A]]
    1.50    }
    1.51 @@ -697,10 +672,10 @@
    1.52        Command.State.merge_results(command_states(version, command))
    1.53  
    1.54      def command_markup(version: Version, command: Command, index: Command.Markup_Index,
    1.55 -        range: Text.Range, elements: Elements): Markup_Tree =
    1.56 +        range: Text.Range, elements: Markup.Elements): Markup_Tree =
    1.57        Command.State.merge_markup(command_states(version, command), index, range, elements)
    1.58  
    1.59 -    def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
    1.60 +    def markup_to_XML(version: Version, node: Node, elements: Markup.Elements): XML.Body =
    1.61        (for {
    1.62          command <- node.commands.iterator
    1.63          markup =
    1.64 @@ -769,7 +744,7 @@
    1.65          def cumulate[A](
    1.66            range: Text.Range,
    1.67            info: A,
    1.68 -          elements: Elements,
    1.69 +          elements: Markup.Elements,
    1.70            result: List[Command.State] => (A, Text.Markup) => Option[A],
    1.71            status: Boolean = false): List[Text.Info[A]] =
    1.72          {
    1.73 @@ -797,7 +772,7 @@
    1.74  
    1.75          def select[A](
    1.76            range: Text.Range,
    1.77 -          elements: Elements,
    1.78 +          elements: Markup.Elements,
    1.79            result: List[Command.State] => Text.Markup => Option[A],
    1.80            status: Boolean = false): List[Text.Info[A]] =
    1.81          {