--- a/src/Pure/Tools/spell_checker.scala Mon Jun 19 19:58:56 2017 +0200
+++ b/src/Pure/Tools/spell_checker.scala Mon Jun 19 19:59:13 2017 +0200
@@ -52,6 +52,15 @@
result.toList
}
+ def current_word(rendering: Rendering, range: Text.Range): Option[Text.Info[String]] =
+ {
+ for {
+ spell_range <- rendering.spell_checker_point(range)
+ text <- rendering.model.try_get_text(spell_range)
+ info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
+ } yield info
+ }
+
/* dictionaries */
--- a/src/Tools/jEdit/src/isabelle.scala Mon Jun 19 19:58:56 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Jun 19 19:59:13 2017 +0200
@@ -419,7 +419,7 @@
doc_view <- Document_View.get(text_area)
rendering = doc_view.get_rendering()
range = JEdit_Lib.caret_range(text_area)
- Text.Info(_, word) <- JEdit_Spell_Checker.current_word(text_area, rendering, range)
+ Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} {
spell_checker.update(word, include, permanent)
JEdit_Lib.jedit_views().foreach(_.repaint())
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Jun 19 19:58:56 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Jun 19 19:59:13 2017 +0200
@@ -19,20 +19,6 @@
object JEdit_Spell_Checker
{
- /* words within text */
-
- def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range)
- : Option[Text.Info[String]] =
- {
- for {
- spell_range <- rendering.spell_checker_point(range)
- text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
- info <- Spell_Checker.marked_words(
- spell_range.start, text, info => info.range.overlaps(range)).headOption
- } yield info
- }
-
-
/* completion */
def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering)
@@ -42,7 +28,7 @@
spell_checker <- PIDE.plugin.spell_checker.get
if explicit
range = JEdit_Lib.before_caret_range(text_area, rendering)
- word <- current_word(text_area, rendering, range)
+ word <- Spell_Checker.current_word(rendering, range)
words = spell_checker.complete(word.info)
if words.nonEmpty
descr = "(from dictionary " + quote(spell_checker.toString) + ")"
@@ -62,7 +48,7 @@
doc_view <- Document_View.get(text_area)
rendering = doc_view.get_rendering()
range = JEdit_Lib.point_range(text_area.getBuffer, offset)
- Text.Info(_, word) <- current_word(text_area, rendering, range)
+ Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} yield (spell_checker, word)
result match {