# HG changeset patch # User wenzelm # Date 1397643972 -7200 # Node ID 8f80a243857deade7a61a95c7dc6ed6805fe98b0 # Parent 628e039cc34d9c9b2ff1ea71e7d7376f097d58d2 clarified word case; more robust treatment of codepoints; diff -r 628e039cc34d -r 8f80a243857d src/Pure/General/word.scala --- a/src/Pure/General/word.scala Wed Apr 16 11:52:26 2014 +0200 +++ b/src/Pure/General/word.scala Wed Apr 16 12:26:12 2014 +0200 @@ -13,6 +13,21 @@ object Word { + /* codepoints */ + + def codepoint_iterator(str: String): Iterator[Int] = + new Iterator[Int] { + var offset = 0 + def hasNext: Boolean = offset < str.length + def next: Int = + { + val c = str.codePointAt(offset) + offset += Character.charCount(c) + c + } + } + + /* case */ def lowercase(str: String): String = str.toLowerCase(Locale.ROOT) @@ -20,7 +35,37 @@ def capitalize(str: String): String = if (str.length == 0) str - else uppercase(str.substring(0, 1)) + str.substring(1) + else { + val n = Character.charCount(str.codePointAt(0)) + uppercase(str.substring(0, n)) + str.substring(n) + } + + sealed abstract class Case + case object Lowercase extends Case + case object Uppercase extends Case + case object Capitalized extends Case + + object Case + { + def apply(c: Case, str: String): String = + c match { + case Lowercase => lowercase(str) + case Uppercase => uppercase(str) + case Capitalized => capitalize(str) + } + def unapply(str: String): Option[Case] = + if (!str.isEmpty) { + if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase) + else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase) + else { + val it = codepoint_iterator(str) + if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_))) + Some(Capitalized) + else None + } + } + else None + } def is_capitalized(str: String): Boolean = str.length > 0 && diff -r 628e039cc34d -r 8f80a243857d src/Tools/jEdit/src/spell_checker.scala --- a/src/Tools/jEdit/src/spell_checker.scala Wed Apr 16 11:52:26 2014 +0200 +++ b/src/Tools/jEdit/src/spell_checker.scala Wed Apr 16 12:26:12 2014 +0200 @@ -247,15 +247,17 @@ } def check(word: String): Boolean = - contains(word) || - Word.is_all_caps(word) && contains(Word.lowercase(word)) || - Word.is_capitalized(word) && - (contains(Word.lowercase(word)) || contains(Word.uppercase(word))) + word match { + case Word.Case(Word.Uppercase) => contains(Word.lowercase(word)) + case Word.Case(Word.Capitalized) => + contains(Word.lowercase(word)) || contains(Word.uppercase(word)) + case _ => contains(word) + } def complete(word: String): List[String] = if (check(word)) Nil else { - val m = dict.getClass.getSuperclass. getDeclaredMethod("searchSuggestions", classOf[String]) + val m = dict.getClass.getSuperclass.getDeclaredMethod("searchSuggestions", classOf[String]) m.setAccessible(true) m.invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString) }