equal
deleted
inserted
replaced
59 } |
59 } |
60 } |
60 } |
61 result.toList |
61 result.toList |
62 } |
62 } |
63 |
63 |
64 def current_word(text_area: TextArea, rendering: Rendering, range: Text.Range) |
64 def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range) |
65 : Option[Text.Info[String]] = |
65 : Option[Text.Info[String]] = |
66 { |
66 { |
67 for { |
67 for { |
68 spell_range <- rendering.spell_checker_point(range) |
68 spell_range <- rendering.spell_checker_point(range) |
69 text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range) |
69 text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range) |
73 |
73 |
74 |
74 |
75 |
75 |
76 /** completion **/ |
76 /** completion **/ |
77 |
77 |
78 def completion(text_area: TextArea, explicit: Boolean, rendering: Rendering) |
78 def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering) |
79 : Option[Completion.Result] = |
79 : Option[Completion.Result] = |
80 { |
80 { |
81 for { |
81 for { |
82 spell_checker <- PIDE.spell_checker.get |
82 spell_checker <- PIDE.spell_checker.get |
83 if explicit |
83 if explicit |