src/Tools/jEdit/src/text_area_painter.scala
changeset 46913 3444a24dc4e9
parent 46817 90c8620852cf
child 47027 fc3bb6c02a3c
equal deleted inserted replaced
46912:e0cd5c4df8e6 46913:3444a24dc4e9
   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)