--- 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))
}