equal
deleted
inserted
replaced
183 var result = Map[Text.Offset, Chunk]() |
183 var result = Map[Text.Offset, Chunk]() |
184 for (line <- physical_lines) { |
184 for (line <- physical_lines) { |
185 val line_start = buffer.getLineStartOffset(line) |
185 val line_start = buffer.getLineStartOffset(line) |
186 |
186 |
187 out.clear |
187 out.clear |
188 handler.init(painter.getStyles, font_context, painter, out, margin) // jedit-4.5.0: line_start |
188 handler.init(painter.getStyles, font_context, painter, out, margin, line_start) |
189 buffer.markTokens(line, handler) |
189 buffer.markTokens(line, handler) |
190 |
190 |
191 for (i <- 0 until out.size) { |
191 for (i <- 0 until out.size) { |
192 val chunk = out.get(i) |
192 val chunk = out.get(i) |
193 result += (line_start + chunk.offset -> chunk) |
193 result += (line_start + chunk.offset -> chunk) |