--- a/src/Tools/jEdit/src/rich_text_area.scala Sun Apr 13 19:32:49 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sun Apr 13 19:55:16 2014 +0200
@@ -322,7 +322,7 @@
spell_checker <- PIDE.spell_checker.get
range0 <- rendering.spell_checker_ranges(line_range)
text <- JEdit_Lib.try_get_text(buffer, range0)
- range <- spell_checker.bad_words(text)
+ range <- spell_checker.marked_words(text)
r <- JEdit_Lib.gfx_range(text_area, range + range0.start)
} {
gfx.setColor(rendering.spell_checker_color)