src/Pure/PIDE/document.scala
changeset 45468 33e946d3f449
parent 45467 3f290b6288cf
child 45474 f793dd5d84b2
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Nov 12 11:45:49 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Nov 12 12:21:42 2011 +0100
     1.3 @@ -241,7 +241,7 @@
     1.4      def revert(i: Text.Offset): Text.Offset
     1.5      def revert(range: Text.Range): Text.Range
     1.6      def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
     1.7 -    def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
     1.8 +    def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
     1.9        : Stream[Text.Info[Option[A]]]
    1.10    }
    1.11  
    1.12 @@ -492,19 +492,16 @@
    1.13            } yield Text.Info(convert(r0 + command_start), a)
    1.14          }
    1.15  
    1.16 -        def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    1.17 +        def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
    1.18            : Stream[Text.Info[Option[A]]] =
    1.19          {
    1.20 -          val former_range = revert(range)
    1.21 -          for {
    1.22 -            (command, command_start) <- node.command_range(former_range).toStream
    1.23 -            Text.Info(r0, x) <- command_state(command).markup.
    1.24 -              select((former_range - command_start).restrict(command.range)) {
    1.25 -                case Text.Info(r0, info)
    1.26 -                if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
    1.27 -                  result(Text.Info(convert(r0 + command_start), info))
    1.28 -              }
    1.29 -          } yield Text.Info(convert(r0 + command_start), x)
    1.30 +          val result = body.result
    1.31 +          val result1 =
    1.32 +            new PartialFunction[(Option[A], Text.Markup), Option[A]] {
    1.33 +              def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
    1.34 +              def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
    1.35 +            }
    1.36 +          cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1))
    1.37          }
    1.38        }
    1.39      }