src/Pure/PIDE/document.scala
changeset 46198 cd040c5772de
parent 46178 1c5c88f6feb5
child 46208 4cab63a6dc16
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Jan 12 21:21:22 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Jan 12 21:50:00 2012 +0100
     1.3 @@ -242,7 +242,7 @@
     1.4      def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
     1.5        result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
     1.6      def select_markup[A](range: Text.Range, elements: Option[Set[String]],
     1.7 -      result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]]
     1.8 +      result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
     1.9    }
    1.10  
    1.11    type Assign =
    1.12 @@ -489,14 +489,15 @@
    1.13          }
    1.14  
    1.15          def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.16 -          result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]] =
    1.17 +          result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
    1.18          {
    1.19            val result1 =
    1.20              new PartialFunction[(Option[A], Text.Markup), Option[A]] {
    1.21                def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
    1.22                def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
    1.23              }
    1.24 -          cumulate_markup(range, None, elements, result1)
    1.25 +          for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
    1.26 +            yield Text.Info(r, x)
    1.27          }
    1.28        }
    1.29      }