tuned signature;
authorwenzelm
Sun, 13 Apr 2014 19:55:16 +0200
changeset 56563 9ac666f343d4
parent 56562 7f6f5665a96e
child 56564 94c55cc73747
tuned signature;
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/spell_checker.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)
--- 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))
 }