equal
deleted
inserted
replaced
297 { |
297 { |
298 for { |
298 for { |
299 spell_checker <- PIDE.spell_checker.get |
299 spell_checker <- PIDE.spell_checker.get |
300 doc_view <- PIDE.document_view(text_area) |
300 doc_view <- PIDE.document_view(text_area) |
301 rendering = doc_view.get_rendering() |
301 rendering = doc_view.get_rendering() |
302 range = JEdit_Lib.before_caret_range(text_area, rendering) |
302 range <- JEdit_Lib.before_caret_range(text_area, rendering) |
303 Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range) |
303 Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range) |
304 } { |
304 } { |
305 spell_checker.update(word, include, permanent) |
305 spell_checker.update(word, include, permanent) |
306 JEdit_Lib.jedit_views().foreach(_.repaint()) |
306 JEdit_Lib.jedit_views().foreach(_.repaint()) |
307 } |
307 } |