author | wenzelm |
Mon, 11 Jul 2016 20:37:28 +0200 | |
changeset 63450 | afd657fffdf9 |
parent 62812 | ce22e5c3d4ce |
child 64370 | 865b39487b5d |
permissions | -rw-r--r-- |
56599 | 1 |
/* Title: Pure/General/word.scala |
56748 | 2 |
Module: PIDE |
56599 | 3 |
Author: Makarius |
4 |
||
56747 | 5 |
Support for words within Unicode text. |
56599 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
62812
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
10 |
import java.text.Bidi |
56599 | 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 |
||
56792 | 30 |
def codepoint(c: Int): String = new String(Array(c), 0, 1) |
31 |
||
56601 | 32 |
|
62812
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
33 |
/* directionality */ |
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
34 |
|
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
35 |
def bidi_detect(str: String): Boolean = |
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
36 |
str.exists(c => c >= 0x590) && Bidi.requiresBidi(str.toArray, 0, str.length) |
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
37 |
|
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
38 |
def bidi_override(str: String): String = |
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
39 |
if (bidi_detect(str)) "\u200E\u202D" + str + "\u202C" else str |
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
40 |
|
ce22e5c3d4ce
more robust display of bidirectional Unicode text: enforce left-to-right;
wenzelm
parents:
59319
diff
changeset
|
41 |
|
56600 | 42 |
/* case */ |
43 |
||
56599 | 44 |
def lowercase(str: String): String = str.toLowerCase(Locale.ROOT) |
45 |
def uppercase(str: String): String = str.toUpperCase(Locale.ROOT) |
|
46 |
||
47 |
def capitalize(str: String): String = |
|
48 |
if (str.length == 0) str |
|
56601 | 49 |
else { |
50 |
val n = Character.charCount(str.codePointAt(0)) |
|
56602 | 51 |
uppercase(str.substring(0, n)) + lowercase(str.substring(n)) |
56601 | 52 |
} |
53 |
||
56609
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56602
diff
changeset
|
54 |
def perhaps_capitalize(str: String): String = |
57087
16536c15d749
capitalize even more carefully (see 5ac67041ccf8), e.g. relevant for option "z3_non_commercial" and prospective "MaSh";
wenzelm
parents:
56792
diff
changeset
|
55 |
if (codepoint_iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c))) |
16536c15d749
capitalize even more carefully (see 5ac67041ccf8), e.g. relevant for option "z3_non_commercial" and prospective "MaSh";
wenzelm
parents:
56792
diff
changeset
|
56 |
capitalize(str) |
16536c15d749
capitalize even more carefully (see 5ac67041ccf8), e.g. relevant for option "z3_non_commercial" and prospective "MaSh";
wenzelm
parents:
56792
diff
changeset
|
57 |
else str |
56609
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56602
diff
changeset
|
58 |
|
56601 | 59 |
sealed abstract class Case |
60 |
case object Lowercase extends Case |
|
61 |
case object Uppercase extends Case |
|
62 |
case object Capitalized extends Case |
|
63 |
||
64 |
object Case |
|
65 |
{ |
|
66 |
def apply(c: Case, str: String): String = |
|
67 |
c match { |
|
68 |
case Lowercase => lowercase(str) |
|
69 |
case Uppercase => uppercase(str) |
|
70 |
case Capitalized => capitalize(str) |
|
71 |
} |
|
72 |
def unapply(str: String): Option[Case] = |
|
59319 | 73 |
if (str.nonEmpty) { |
56601 | 74 |
if (codepoint_iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase) |
75 |
else if (codepoint_iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase) |
|
76 |
else { |
|
77 |
val it = codepoint_iterator(str) |
|
78 |
if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_))) |
|
79 |
Some(Capitalized) |
|
80 |
else None |
|
81 |
} |
|
82 |
} |
|
83 |
else None |
|
84 |
} |
|
56599 | 85 |
|
56600 | 86 |
|
87 |
/* sequence of words */ |
|
88 |
||
89 |
def implode(words: Iterable[String]): String = words.iterator.mkString(" ") |
|
90 |
||
91 |
def explode(sep: Char => Boolean, text: String): List[String] = |
|
92 |
Library.separated_chunks(sep, text).map(_.toString).filter(_ != "").toList |
|
93 |
||
94 |
def explode(sep: Char, text: String): List[String] = |
|
95 |
explode(_ == sep, text) |
|
96 |
||
97 |
def explode(text: String): List[String] = |
|
56747 | 98 |
explode(Character.isWhitespace(_), text) |
63450 | 99 |
|
100 |
||
101 |
/* brackets */ |
|
102 |
||
103 |
val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃" |
|
104 |
val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄" |
|
56599 | 105 |
} |