src/Pure/PIDE/document.scala
changeset 56354 a6f8c3566560
parent 56337 520148f9921d
child 56372 fadb0fef09d7
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Apr 01 17:29:47 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Apr 01 20:22:25 2014 +0200
     1.3 @@ -434,13 +434,13 @@
     1.4        range: Text.Range,
     1.5        info: A,
     1.6        elements: Elements,
     1.7 -      result: Command.Results => (A, Text.Markup) => Option[A],
     1.8 +      result: List[Command.State] => (A, Text.Markup) => Option[A],
     1.9        status: Boolean = false): List[Text.Info[A]]
    1.10  
    1.11      def select[A](
    1.12        range: Text.Range,
    1.13        elements: Elements,
    1.14 -      result: Command.Results => Text.Markup => Option[A],
    1.15 +      result: List[Command.State] => Text.Markup => Option[A],
    1.16        status: Boolean = false): List[Text.Info[A]]
    1.17    }
    1.18  
    1.19 @@ -729,7 +729,7 @@
    1.20            range: Text.Range,
    1.21            info: A,
    1.22            elements: Elements,
    1.23 -          result: Command.Results => (A, Text.Markup) => Option[A],
    1.24 +          result: List[Command.State] => (A, Text.Markup) => Option[A],
    1.25            status: Boolean = false): List[Text.Info[A]] =
    1.26          {
    1.27            val former_range = revert(range)
    1.28 @@ -743,7 +743,7 @@
    1.29              (command, command_start) <- command_range_iterator
    1.30              chunk <- command.chunks.get(file_name).iterator
    1.31              states = state.command_states(version, command)
    1.32 -            res = result(Command.State.merge_results(states))
    1.33 +            res = result(states)
    1.34              range = (former_range - command_start).restrict(chunk.range)
    1.35              markup = Command.State.merge_markup(states, markup_index, range, elements)
    1.36              Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
    1.37 @@ -756,12 +756,12 @@
    1.38          def select[A](
    1.39            range: Text.Range,
    1.40            elements: Elements,
    1.41 -          result: Command.Results => Text.Markup => Option[A],
    1.42 +          result: List[Command.State] => Text.Markup => Option[A],
    1.43            status: Boolean = false): List[Text.Info[A]] =
    1.44          {
    1.45 -          def result1(results: Command.Results): (Option[A], Text.Markup) => Option[Option[A]] =
    1.46 +          def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] =
    1.47            {
    1.48 -            val res = result(results)
    1.49 +            val res = result(states)
    1.50              (_: Option[A], x: Text.Markup) =>
    1.51                res(x) match {
    1.52                  case None => None