src/Pure/PIDE/document.scala
changeset 45467 3f290b6288cf
parent 45459 a5c1599f664d
child 45468 33e946d3f449
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Nov 11 22:09:07 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Nov 12 11:45:49 2011 +0100
     1.3 @@ -240,8 +240,7 @@
     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](info: Text.Info[A])(result: Markup_Tree.Cumulate[A])
     1.8 -      : Stream[Text.Info[A]]
     1.9 +    def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
    1.10      def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    1.11        : Stream[Text.Info[Option[A]]]
    1.12    }
    1.13 @@ -473,18 +472,23 @@
    1.14          def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    1.15          def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    1.16  
    1.17 -        def cumulate_markup[A](root: Text.Info[A])(result: Markup_Tree.Cumulate[A])
    1.18 +        def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A])
    1.19            : Stream[Text.Info[A]] =
    1.20          {
    1.21 -          val former_range = revert(root.range)
    1.22 +          val info = body.info
    1.23 +          val result = body.result
    1.24 +
    1.25 +          val former_range = revert(range)
    1.26            for {
    1.27              (command, command_start) <- node.command_range(former_range).toStream
    1.28              Text.Info(r0, a) <- command_state(command).markup.
    1.29 -              cumulate(Text.Info((former_range - command_start).restrict(command.range), root.info)) {
    1.30 -                case (a, Text.Info(r0, b))
    1.31 -                if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.32 -                  result((a, Text.Info(convert(r0 + command_start), b)))
    1.33 -              }
    1.34 +              cumulate((former_range - command_start).restrict(command.range))(
    1.35 +                Markup_Tree.Cumulate[A](info,
    1.36 +                  {
    1.37 +                    case (a, Text.Info(r0, b))
    1.38 +                    if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.39 +                      result((a, Text.Info(convert(r0 + command_start), b)))
    1.40 +                  }))
    1.41            } yield Text.Info(convert(r0 + command_start), a)
    1.42          }
    1.43