src/Pure/PIDE/document.scala
changeset 50500 c94bba7906d2
parent 50204 daeb1674fb91
child 51293 05b1bbae748d
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Dec 12 23:36:07 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Dec 13 13:52:18 2012 +0100
     1.3 @@ -280,9 +280,9 @@
     1.4      def revert(range: Text.Range): Text.Range
     1.5      def eq_markup(other: Snapshot): Boolean
     1.6      def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
     1.7 -      result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
     1.8 +      result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
     1.9      def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.10 -      result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
    1.11 +      result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
    1.12    }
    1.13  
    1.14    type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])]  // exec state assignment
    1.15 @@ -506,29 +506,34 @@
    1.16              })
    1.17  
    1.18          def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
    1.19 -          result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
    1.20 +          result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
    1.21          {
    1.22            val former_range = revert(range)
    1.23            for {
    1.24              (command, command_start) <- node.command_range(former_range).toStream
    1.25 -            Text.Info(r0, a) <- state.command_state(version, command).markup.
    1.26 +            st = state.command_state(version, command)
    1.27 +            res = result(st)
    1.28 +            Text.Info(r0, a) <- st.markup.
    1.29                cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
    1.30                  {
    1.31                    case (a, Text.Info(r0, b))
    1.32 -                  if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.33 -                    result((a, Text.Info(convert(r0 + command_start), b)))
    1.34 +                  if res.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.35 +                    res((a, Text.Info(convert(r0 + command_start), b)))
    1.36                  })
    1.37            } yield Text.Info(convert(r0 + command_start), a)
    1.38          }
    1.39  
    1.40          def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.41 -          result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
    1.42 +          result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
    1.43          {
    1.44 -          val result1 =
    1.45 +          def result1(st: Command.State) =
    1.46 +          {
    1.47 +            val res = result(st)
    1.48              new PartialFunction[(Option[A], Text.Markup), Option[A]] {
    1.49 -              def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
    1.50 -              def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
    1.51 +              def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = res.isDefinedAt(arg._2)
    1.52 +              def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(res(arg._2))
    1.53              }
    1.54 +          }
    1.55            for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
    1.56              yield Text.Info(r, x)
    1.57          }