# HG changeset patch
# User wenzelm
# Date 1397411716 -7200
# Node ID 9ac666f343d4182edb2a1569fe1aee2640569e4a
# Parent  7f6f5665a96ed6e35969daf208cc61d660add54a
tuned signature;

diff -r 7f6f5665a96e -r 9ac666f343d4 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Apr 13 19:32:49 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Apr 13 19:55:16 2014 +0200
@@ -322,7 +322,7 @@
               spell_checker <- PIDE.spell_checker.get
               range0 <- rendering.spell_checker_ranges(line_range)
               text <- JEdit_Lib.try_get_text(buffer, range0)
-              range <- spell_checker.bad_words(text)
+              range <- spell_checker.marked_words(text)
               r <- JEdit_Lib.gfx_range(text_area, range + range0.start)
             } {
               gfx.setColor(rendering.spell_checker_color)
diff -r 7f6f5665a96e -r 9ac666f343d4 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Sun Apr 13 19:32:49 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Sun Apr 13 19:55:16 2014 +0200
@@ -20,6 +20,39 @@
 
 object Spell_Checker
 {
+  /* marked words within text */
+
+  def marked_words(text: String, mark: String => Boolean): List[Text.Range] =
+  {
+    val result = new mutable.ListBuffer[Text.Range]
+    var offset = 0
+
+    def apostrophe(c: Int): Boolean =
+      c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
+
+    @tailrec def scan(pred: Int => Boolean)
+    {
+      if (offset < text.length) {
+        val c = text.codePointAt(offset)
+        if (pred(c)) {
+          offset += Character.charCount(c)
+          scan(pred)
+        }
+      }
+    }
+
+    while (offset < text.length) {
+      scan(c => !Character.isLetter(c))
+      val start = offset
+      scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
+      val stop = offset
+      if (stop - start >= 2 && mark(text.substring(start, stop)))
+        result += Text.Range(start, stop)
+    }
+    result.toList
+  }
+
+
   /* dictionary consisting of word list */
 
   class Dictionary private [Spell_Checker](path: Path)
@@ -133,35 +166,8 @@
     m.invoke(dictionary, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
   }
 
-  def bad_words(text: String): List[Text.Range] =
-  {
-    val result = new mutable.ListBuffer[Text.Range]
-    var offset = 0
-
-    def apostrophe(c: Int): Boolean =
-      c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
-
-    @tailrec def scan(pred: Int => Boolean)
-    {
-      if (offset < text.length) {
-        val c = text.codePointAt(offset)
-        if (pred(c)) {
-          offset += Character.charCount(c)
-          scan(pred)
-        }
-      }
-    }
-
-    while (offset < text.length) {
-      scan(c => !Character.isLetter(c))
-      val start = offset
-      scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
-      val stop = offset
-      if (stop - start >= 2 && !check(text.substring(start, stop)))
-        result += Text.Range(start, stop)
-    }
-    result.toList
-  }
+  def marked_words(text: String): List[Text.Range] =
+    Spell_Checker.marked_words(text, w => !check(w))
 }