equal
deleted
inserted
replaced
320 // spell checker |
320 // spell checker |
321 for { |
321 for { |
322 spell_checker <- PIDE.spell_checker.get |
322 spell_checker <- PIDE.spell_checker.get |
323 range0 <- rendering.spell_checker_ranges(line_range) |
323 range0 <- rendering.spell_checker_ranges(line_range) |
324 text <- JEdit_Lib.try_get_text(buffer, range0) |
324 text <- JEdit_Lib.try_get_text(buffer, range0) |
325 range <- spell_checker.bad_words(text) |
325 range <- spell_checker.marked_words(text) |
326 r <- JEdit_Lib.gfx_range(text_area, range + range0.start) |
326 r <- JEdit_Lib.gfx_range(text_area, range + range0.start) |
327 } { |
327 } { |
328 gfx.setColor(rendering.spell_checker_color) |
328 gfx.setColor(rendering.spell_checker_color) |
329 val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2)) |
329 val y0 = r.y + ((fm.getAscent + 4) min (line_height - 2)) |
330 gfx.drawLine(r.x, y0, r.x + r.length, y0) |
330 gfx.drawLine(r.x, y0, r.x + r.length, y0) |