49322
|
1 |
/* Title: Pure/System/color_value.scala
|
49294
|
2 |
Module: PIDE
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Cached color values.
|
|
6 |
*/
|
|
7 |
|
|
8 |
package isabelle
|
|
9 |
|
|
10 |
|
|
11 |
import java.awt.Color
|
|
12 |
|
|
13 |
|
|
14 |
object Color_Value
|
|
15 |
{
|
|
16 |
private var cache = Map.empty[String, Color]
|
|
17 |
|
|
18 |
def parse(s: String): Color =
|
|
19 |
{
|
|
20 |
val i = java.lang.Long.parseLong(s, 16)
|
|
21 |
val r = ((i >> 24) & 0xFF).toInt
|
|
22 |
val g = ((i >> 16) & 0xFF).toInt
|
|
23 |
val b = ((i >> 8) & 0xFF).toInt
|
|
24 |
val a = (i & 0xFF).toInt
|
|
25 |
new Color(r, g, b, a)
|
|
26 |
}
|
|
27 |
|
|
28 |
def print(c: Color): String =
|
|
29 |
{
|
|
30 |
val r = new java.lang.Integer(c.getRed)
|
|
31 |
val g = new java.lang.Integer(c.getGreen)
|
|
32 |
val b = new java.lang.Integer(c.getBlue)
|
|
33 |
val a = new java.lang.Integer(c.getAlpha)
|
|
34 |
String.format("%02x%02x%02x%02x", r, g, b, a).toUpperCase
|
|
35 |
}
|
|
36 |
|
|
37 |
def apply(s: String): Color =
|
|
38 |
synchronized {
|
|
39 |
cache.get(s) match {
|
|
40 |
case Some(c) => c
|
|
41 |
case None =>
|
|
42 |
val c = parse(s)
|
|
43 |
cache += (s -> c)
|
|
44 |
c
|
|
45 |
}
|
|
46 |
}
|
|
47 |
}
|
|
48 |
|