src/Pure/PIDE/document.scala
changeset 56301 1da7b4c33db9
parent 56300 8346b664fa7a
child 56309 5003ea266aef
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Mar 27 11:19:31 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 27 12:11:32 2014 +0100
     1.3 @@ -650,13 +650,15 @@
     1.4      def command_results(version: Version, command: Command): Command.Results =
     1.5        Command.State.merge_results(command_states(version, command))
     1.6  
     1.7 -    def command_markup(version: Version, command: Command, index: Command.Markup_Index): Markup_Tree =
     1.8 -      Command.State.merge_markup(command_states(version, command), index)
     1.9 +    def command_markup(version: Version, command: Command, index: Command.Markup_Index,
    1.10 +        range: Text.Range, elements: Elements): Markup_Tree =
    1.11 +      Command.State.merge_markup(command_states(version, command), index, range, elements)
    1.12  
    1.13      def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
    1.14        (for {
    1.15          command <- node.commands.iterator
    1.16 -        markup = command_markup(version, command, Command.Markup_Index.markup)
    1.17 +        markup =
    1.18 +          command_markup(version, command, Command.Markup_Index.markup, command.range, elements)
    1.19          tree <- markup.to_XML(command.range, command.source, elements)
    1.20        } yield tree).toList
    1.21  
    1.22 @@ -734,8 +736,9 @@
    1.23                  chunk <- thy_load_command.chunks.get(file_name).iterator
    1.24                  states = state.command_states(version, thy_load_command)
    1.25                  res = result(Command.State.merge_results(states))
    1.26 -                Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
    1.27 -                  former_range.restrict(chunk.range), info, elements,
    1.28 +                range = former_range.restrict(chunk.range)
    1.29 +                markup = Command.State.merge_markup(states, markup_index, range, elements)
    1.30 +                Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
    1.31                    { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    1.32                  ).iterator
    1.33                } yield Text.Info(convert(r0), a)).toList
    1.34 @@ -746,8 +749,9 @@
    1.35                  (command, command_start) <- node.command_range(former_range)
    1.36                  states = state.command_states(version, command)
    1.37                  res = result(Command.State.merge_results(states))
    1.38 -                Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
    1.39 -                  (former_range - command_start).restrict(command.range), info, elements,
    1.40 +                range = (former_range - command_start).restrict(command.range)
    1.41 +                markup = Command.State.merge_markup(states, markup_index, range, elements)
    1.42 +                Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
    1.43                    {
    1.44                      case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
    1.45                    }).iterator