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