src/Pure/PIDE/document.scala
changeset 55650 349afd0fa0c4
parent 55649 1532ab0dc67b
child 55651 fa42cf3fe79b
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Feb 21 15:12:50 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Feb 21 15:22:06 2014 +0100
     1.3 @@ -659,7 +659,7 @@
     1.4                  chunk <- thy_load_command.chunks.get(file_name).iterator
     1.5                  st = state.command_state(version, thy_load_command)
     1.6                  res = result(st)
     1.7 -                Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
     1.8 +                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
     1.9                    former_range.restrict(chunk.range), info, elements,
    1.10                    { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    1.11                  ).iterator
    1.12 @@ -671,7 +671,7 @@
    1.13                  (command, command_start) <- node.command_range(former_range)
    1.14                  st = state.command_state(version, command)
    1.15                  res = result(st)
    1.16 -                Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
    1.17 +                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
    1.18                    (former_range - command_start).restrict(command.range), info, elements,
    1.19                    {
    1.20                      case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))