src/Pure/PIDE/document.scala
changeset 56298 cf7710540f39
parent 56295 a40e67ce4f84
child 56299 8201790fdeb9
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Mar 26 20:32:15 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Mar 26 21:01:09 2014 +0100
     1.3 @@ -429,13 +429,13 @@
     1.4        range: Text.Range,
     1.5        info: A,
     1.6        elements: Elements,
     1.7 -      result: Command.State => (A, Text.Markup) => Option[A],
     1.8 +      result: Command.Results => (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.State => Text.Markup => Option[A],
    1.15 +      result: Command.Results => Text.Markup => Option[A],
    1.16        status: Boolean = false): List[Text.Info[A]]
    1.17    }
    1.18  
    1.19 @@ -708,7 +708,7 @@
    1.20            range: Text.Range,
    1.21            info: A,
    1.22            elements: Elements,
    1.23 -          result: Command.State => (A, Text.Markup) => Option[A],
    1.24 +          result: Command.Results => (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 @@ -719,7 +719,7 @@
    1.29                (for {
    1.30                  chunk <- thy_load_command.chunks.get(file_name).iterator
    1.31                  st = state.command_state(version, thy_load_command)
    1.32 -                res = result(st)
    1.33 +                res = result(st.results)
    1.34                  Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
    1.35                    former_range.restrict(chunk.range), info, elements,
    1.36                    { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    1.37 @@ -731,7 +731,7 @@
    1.38                (for {
    1.39                  (command, command_start) <- node.command_range(former_range)
    1.40                  st = state.command_state(version, command)
    1.41 -                res = result(st)
    1.42 +                res = result(st.results)
    1.43                  Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
    1.44                    (former_range - command_start).restrict(command.range), info, elements,
    1.45                    {
    1.46 @@ -744,12 +744,12 @@
    1.47          def select[A](
    1.48            range: Text.Range,
    1.49            elements: Elements,
    1.50 -          result: Command.State => Text.Markup => Option[A],
    1.51 +          result: Command.Results => Text.Markup => Option[A],
    1.52            status: Boolean = false): List[Text.Info[A]] =
    1.53          {
    1.54 -          def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
    1.55 +          def result1(results: Command.Results): (Option[A], Text.Markup) => Option[Option[A]] =
    1.56            {
    1.57 -            val res = result(st)
    1.58 +            val res = result(results)
    1.59              (_: Option[A], x: Text.Markup) =>
    1.60                res(x) match {
    1.61                  case None => None