src/Pure/General/word.scala

clarified word case;
more robust treatment of codepoints;

/*  Title:      Pure/General/word.scala
    Module:     PIDE
    Author:     Makarius

Support for plain text words.
*/

package isabelle


import java.util.Locale


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)
  def uppercase(str: String): String = str.toUpperCase(Locale.ROOT)

  def capitalize(str: String): String =
    if (str.length == 0) str
    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 &&
    Character.isUpperCase(str(0)) && str.substring(1).forall(Character.isLowerCase(_))

  def is_all_caps(str: String): Boolean =
    str.length > 0 && str.forall(Character.isUpperCase(_))


  /* sequence of words */

  def implode(words: Iterable[String]): String = words.iterator.mkString(" ")

  def explode(sep: Char => Boolean, text: String): List[String] =
    Library.separated_chunks(sep, text).map(_.toString).filter(_ != "").toList

  def explode(sep: Char, text: String): List[String] =
    explode(_ == sep, text)

  def explode(text: String): List[String] =
    explode(Symbol.is_ascii_blank(_), text)
}