# HG changeset patch
# User wenzelm
# Date 1497895153 -7200
# Node ID dad409cd3423c205bd638cff39441698709e3b4d
# Parent  135bf45026ea754ab108d6c3ba6d91b1c3a8d8a4
clarified modules;

diff -r 135bf45026ea -r dad409cd3423 src/Pure/Tools/spell_checker.scala
--- 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 */
 
diff -r 135bf45026ea -r dad409cd3423 src/Tools/jEdit/src/isabelle.scala
--- 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())
diff -r 135bf45026ea -r dad409cd3423 src/Tools/jEdit/src/jedit_spell_checker.scala
--- 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 {