author | wenzelm |
Thu, 17 Apr 2014 10:54:10 +0200 | |
changeset 56609 | 5ac67041ccf8 |
parent 56602 | e7e20d72756a |
child 56610 | 5780bddbe9a1 |
permissions | -rw-r--r-- |
56599 | 1 |
/* Title: Pure/General/word.scala |
2 |
Module: PIDE |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Support for plain text words. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
11 |
import java.util.Locale |
|
12 |
||
13 |
||
14 |
object Word |
|
15 |
{ |
|
56601 | 16 |
/* codepoints */ |
17 |
||
18 |
def codepoint_iterator(str: String): Iterator[Int] = |
|
19 |
new Iterator[Int] { |
|
20 |
var offset = 0 |
|
21 |
def hasNext: Boolean = offset < str.length |
|
22 |
def next: Int = |
|
23 |
{ |
|
24 |
val c = str.codePointAt(offset) |
|
25 |
offset += Character.charCount(c) |
|
26 |
c |
|
27 |
} |
|
28 |
} |
|
29 |
||
30 |
||
56600 | 31 |
/* case */ |
32 |
||
56599 | 33 |
def lowercase(str: String): String = str.toLowerCase(Locale.ROOT) |
34 |
def uppercase(str: String): String = str.toUpperCase(Locale.ROOT) |
|
35 |
||
36 |
def capitalize(str: String): String = |
|
37 |
if (str.length == 0) str |
|
56601 | 38 |
else { |
39 |
val n = Character.charCount(str.codePointAt(0)) |
|
56602 | 40 |
uppercase(str.substring(0, n)) + lowercase(str.substring(n)) |
56601 | 41 |
} |
42 |
||
56609
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56602
diff
changeset
|
43 |
def perhaps_capitalize(str: String): String = |
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56602
diff
changeset
|
44 |
str match { |
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56602
diff
changeset
|
45 |
case Case(c) if c != Lowercase => str |
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56602
diff
changeset
|
46 |
case _ => capitalize(str) |
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56602
diff
changeset
|
47 |
} |
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56602
diff
changeset
|
48 |
|
56601 | 49 |
sealed abstract class Case |
50 |
case object Lowercase extends Case |
|
51 |
case object Uppercase extends Case |
|
52 |
case object Capitalized extends Case |
|
53 |
||
54 |
object Case |
|
55 |
{ |
|
56 |
def apply(c: Case, str: String): String = |
|
57 |
c match { |
|
58 |
case Lowercase => lowercase(str) |
|
59 |
case Uppercase => uppercase(str) |
|
60 |
case Capitalized => capitalize(str) |
|
61 |
} |
|
62 |
def unapply(str: String): Option[Case] = |
|
63 |
if (!str.isEmpty) { |
|
64 |
if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase) |
|
65 |
else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase) |
|
66 |
else { |
|
67 |
val it = codepoint_iterator(str) |
|
68 |
if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_))) |
|
69 |
Some(Capitalized) |
|
70 |
else None |
|
71 |
} |
|
72 |
} |
|
73 |
else None |
|
74 |
} |
|
56599 | 75 |
|
76 |
def is_capitalized(str: String): Boolean = |
|
77 |
str.length > 0 && |
|
78 |
Character.isUpperCase(str(0)) && str.substring(1).forall(Character.isLowerCase(_)) |
|
79 |
||
80 |
def is_all_caps(str: String): Boolean = |
|
81 |
str.length > 0 && str.forall(Character.isUpperCase(_)) |
|
82 |
||
56600 | 83 |
|
84 |
/* sequence of words */ |
|
85 |
||
86 |
def implode(words: Iterable[String]): String = words.iterator.mkString(" ") |
|
87 |
||
88 |
def explode(sep: Char => Boolean, text: String): List[String] = |
|
89 |
Library.separated_chunks(sep, text).map(_.toString).filter(_ != "").toList |
|
90 |
||
91 |
def explode(sep: Char, text: String): List[String] = |
|
92 |
explode(_ == sep, text) |
|
93 |
||
94 |
def explode(text: String): List[String] = |
|
95 |
explode(Symbol.is_ascii_blank(_), text) |
|
56599 | 96 |
} |
97 |