src/Pure/PIDE/document.scala
changeset 45459 a5c1599f664d
parent 45243 27466646a7a3
child 45467 3f290b6288cf
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Nov 11 16:25:32 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Nov 11 21:45:52 2011 +0100
     1.3 @@ -240,6 +240,8 @@
     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 select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    1.10        : Stream[Text.Info[Option[A]]]
    1.11    }
    1.12 @@ -471,6 +473,21 @@
    1.13          def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    1.14          def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    1.15  
    1.16 +        def cumulate_markup[A](root: Text.Info[A])(result: Markup_Tree.Cumulate[A])
    1.17 +          : Stream[Text.Info[A]] =
    1.18 +        {
    1.19 +          val former_range = revert(root.range)
    1.20 +          for {
    1.21 +            (command, command_start) <- node.command_range(former_range).toStream
    1.22 +            Text.Info(r0, a) <- command_state(command).markup.
    1.23 +              cumulate(Text.Info((former_range - command_start).restrict(command.range), root.info)) {
    1.24 +                case (a, Text.Info(r0, b))
    1.25 +                if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.26 +                  result((a, Text.Info(convert(r0 + command_start), b)))
    1.27 +              }
    1.28 +          } yield Text.Info(convert(r0 + command_start), a)
    1.29 +        }
    1.30 +
    1.31          def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    1.32            : Stream[Text.Info[Option[A]]] =
    1.33          {