equal
deleted
inserted
replaced
124 var next_x = start |
124 var next_x = start |
125 var cmd = document.command_at(from(start)) |
125 var cmd = document.command_at(from(start)) |
126 while (cmd.isDefined && cmd.get.start(document) < from(stop)) { |
126 while (cmd.isDefined && cmd.get.start(document) < from(stop)) { |
127 val command = cmd.get |
127 val command = cmd.get |
128 for { |
128 for { |
129 markup <- command.highlight_node(document).flatten |
129 markup <- command.highlight(document).flatten |
130 command_start = command.start(document) |
130 command_start = command.start(document) |
131 abs_start = to(command_start + markup.start) |
131 abs_start = to(command_start + markup.start) |
132 abs_stop = to(command_start + markup.stop) |
132 abs_stop = to(command_start + markup.stop) |
133 if (abs_stop > start) |
133 if (abs_stop > start) |
134 if (abs_start < stop) |
134 if (abs_start < stop) |