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