1/*  Title:      Pure/General/word.scala
2    Author:     Makarius
3
4Support for words within Unicode text.
5*/
6
7package isabelle
8
9import java.text.Bidi
10import java.util.Locale
11
12
13object Word
14{
15  /* directionality */
16
17  def bidi_detect(str: String): Boolean =
18    str.exists(c => c >= 0x590) && Bidi.requiresBidi(str.toArray, 0, str.length)
19
20  def bidi_override(str: String): String =
21    if (bidi_detect(str)) "\u200E\u202D" + str + "\u202C" else str
22
23
24  /* case */
25
26  def lowercase(str: String): String = str.toLowerCase(Locale.ROOT)
27  def uppercase(str: String): String = str.toUpperCase(Locale.ROOT)
28
29  def capitalize(str: String): String =
30    if (str.length == 0) str
31    else {
32      val n = Character.charCount(str.codePointAt(0))
33      uppercase(str.substring(0, n)) + lowercase(str.substring(n))
34    }
35
36  def perhaps_capitalize(str: String): String =
37    if (Codepoint.iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c)))
38      capitalize(str)
39    else str
40
41  sealed abstract class Case
42  case object Lowercase extends Case
43  case object Uppercase extends Case
44  case object Capitalized extends Case
45
46  object Case
47  {
48    def apply(c: Case, str: String): String =
49      c match {
50        case Lowercase => lowercase(str)
51        case Uppercase => uppercase(str)
52        case Capitalized => capitalize(str)
53      }
54    def unapply(str: String): Option[Case] =
55      if (str.nonEmpty) {
56        if (Codepoint.iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
57        else if (Codepoint.iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
58        else {
59          val it = Codepoint.iterator(str)
60          if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_)))
61            Some(Capitalized)
62          else None
63        }
64      }
65      else None
66  }
67
68
69  /* sequence of words */
70
71  def implode(words: Iterable[String]): String = words.iterator.mkString(" ")
72
73  def explode(sep: Char => Boolean, text: String): List[String] =
74    Library.separated_chunks(sep, text).map(_.toString).filter(_ != "").toList
75
76  def explode(sep: Char, text: String): List[String] =
77    explode(_ == sep, text)
78
79  def explode(text: String): List[String] =
80    explode(Character.isWhitespace(_), text)
81
82
83  /* brackets */
84
85  val open_brackets = "([{�����������������������"
86  val close_brackets = ")]}�����������������������"
87}
88