src/Pure/PIDE/document.scala
changeset 55820 61869776ce1f
parent 55801 28b59620f0d0
child 56176 0bc9b0ad6287
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Mar 01 09:34:08 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Mar 01 12:07:26 2014 +0100
     1.3 @@ -376,8 +376,32 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* markup elements */
     1.8  
     1.9 -  /** global state -- document structure, execution process, editing history **/
    1.10 +  object Elements
    1.11 +  {
    1.12 +    def apply(elems: Set[String]): Elements = new Elements(elems)
    1.13 +    def apply(elems: String*): Elements = apply(Set(elems: _*))
    1.14 +    val empty: Elements = apply()
    1.15 +    val full: Elements = new Full_Elements
    1.16 +  }
    1.17 +
    1.18 +  sealed class Elements private[Document](private val rep: Set[String])
    1.19 +  {
    1.20 +    def apply(elem: String): Boolean = rep.contains(elem)
    1.21 +    def + (elem: String): Elements = new Elements(rep + elem)
    1.22 +    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
    1.23 +    override def toString: String = rep.mkString("Elements(", ",", ")")
    1.24 +  }
    1.25 +
    1.26 +  private class Full_Elements extends Elements(Set.empty)
    1.27 +  {
    1.28 +    override def apply(elem: String): Boolean = true
    1.29 +    override def toString: String = "Full_Elements()"
    1.30 +  }
    1.31 +
    1.32 +
    1.33 +  /* snapshot */
    1.34  
    1.35    object Snapshot
    1.36    {
    1.37 @@ -403,17 +427,21 @@
    1.38      def cumulate[A](
    1.39        range: Text.Range,
    1.40        info: A,
    1.41 -      elements: String => Boolean,
    1.42 +      elements: Elements,
    1.43        result: Command.State => (A, Text.Markup) => Option[A],
    1.44        status: Boolean = false): List[Text.Info[A]]
    1.45  
    1.46      def select[A](
    1.47        range: Text.Range,
    1.48 -      elements: String => Boolean,
    1.49 +      elements: Elements,
    1.50        result: Command.State => Text.Markup => Option[A],
    1.51        status: Boolean = false): List[Text.Info[A]]
    1.52    }
    1.53  
    1.54 +
    1.55 +
    1.56 +  /** global state -- document structure, execution process, editing history **/
    1.57 +
    1.58    type Assign_Update =
    1.59      List[(Document_ID.Command, List[Document_ID.Exec])]  // update of exec state assignment
    1.60  
    1.61 @@ -672,7 +700,7 @@
    1.62          def cumulate[A](
    1.63            range: Text.Range,
    1.64            info: A,
    1.65 -          elements: String => Boolean,
    1.66 +          elements: Elements,
    1.67            result: Command.State => (A, Text.Markup) => Option[A],
    1.68            status: Boolean = false): List[Text.Info[A]] =
    1.69          {
    1.70 @@ -708,7 +736,7 @@
    1.71  
    1.72          def select[A](
    1.73            range: Text.Range,
    1.74 -          elements: String => Boolean,
    1.75 +          elements: Elements,
    1.76            result: Command.State => Text.Markup => Option[A],
    1.77            status: Boolean = false): List[Text.Info[A]] =
    1.78          {