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