equal
deleted
inserted
replaced
98 def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = |
98 def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = |
99 { |
99 { |
100 val result = |
100 val result = |
101 for { |
101 for { |
102 spell_checker <- PIDE.spell_checker.get |
102 spell_checker <- PIDE.spell_checker.get |
103 doc_view <- PIDE.document_view(text_area) |
103 doc_view <- Document_View.get(text_area) |
104 rendering = doc_view.get_rendering() |
104 rendering = doc_view.get_rendering() |
105 range = JEdit_Lib.point_range(text_area.getBuffer, offset) |
105 range = JEdit_Lib.point_range(text_area.getBuffer, offset) |
106 Text.Info(_, word) <- current_word(text_area, rendering, range) |
106 Text.Info(_, word) <- current_word(text_area, rendering, range) |
107 } yield (spell_checker, word) |
107 } yield (spell_checker, word) |
108 |
108 |