src/Pure/PIDE/document.scala
changeset 46178 1c5c88f6feb5
parent 46152 793cecd4ffc0
child 46198 cd040c5772de
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Jan 10 18:12:55 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Jan 10 23:26:27 2012 +0100
     1.3 @@ -239,9 +239,10 @@
     1.4      def convert(range: Text.Range): Text.Range
     1.5      def revert(i: Text.Offset): Text.Offset
     1.6      def revert(range: Text.Range): Text.Range
     1.7 -    def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
     1.8 -    def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
     1.9 -      : Stream[Text.Info[Option[A]]]
    1.10 +    def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
    1.11 +      result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
    1.12 +    def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.13 +      result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]]
    1.14    }
    1.15  
    1.16    type Assign =
    1.17 @@ -471,37 +472,31 @@
    1.18          def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    1.19          def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    1.20  
    1.21 -        def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A])
    1.22 -          : Stream[Text.Info[A]] =
    1.23 +        def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
    1.24 +          result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
    1.25          {
    1.26 -          val info = body.info
    1.27 -          val result = body.result
    1.28 -
    1.29            val former_range = revert(range)
    1.30            for {
    1.31              (command, command_start) <- node.command_range(former_range).toStream
    1.32              Text.Info(r0, a) <- command_state(command).markup.
    1.33 -              cumulate((former_range - command_start).restrict(command.range))(
    1.34 -                Markup_Tree.Cumulate[A](info,
    1.35 -                  {
    1.36 -                    case (a, Text.Info(r0, b))
    1.37 -                    if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.38 -                      result((a, Text.Info(convert(r0 + command_start), b)))
    1.39 -                  },
    1.40 -                  body.elements))
    1.41 +              cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
    1.42 +                {
    1.43 +                  case (a, Text.Info(r0, b))
    1.44 +                  if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.45 +                    result((a, Text.Info(convert(r0 + command_start), b)))
    1.46 +                })
    1.47            } yield Text.Info(convert(r0 + command_start), a)
    1.48          }
    1.49  
    1.50 -        def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
    1.51 -          : Stream[Text.Info[Option[A]]] =
    1.52 +        def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.53 +          result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]] =
    1.54          {
    1.55 -          val result = body.result
    1.56            val result1 =
    1.57              new PartialFunction[(Option[A], Text.Markup), Option[A]] {
    1.58                def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
    1.59                def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
    1.60              }
    1.61 -          cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1, body.elements))
    1.62 +          cumulate_markup(range, None, elements, result1)
    1.63          }
    1.64        }
    1.65      }