| author | wenzelm | 
| Sun, 11 Oct 2020 13:03:22 +0200 | |
| changeset 72439 | 7f6800b2e8c2 | 
| parent 71381 | b9ea2467c929 | 
| child 75393 | 87ebf5a50283 | 
| permissions | -rw-r--r-- | 
| 53783 
f5e9d182f645
clarified location of GUI modules (which depend on Swing of JFX);
 wenzelm parents: 
49322diff
changeset | 1 | /* Title: Pure/GUI/color_value.scala | 
| 49294 | 2 | Author: Makarius | 
| 3 | ||
| 4 | Cached color values. | |
| 5 | */ | |
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 10 | import java.awt.Color | |
| 62570 | 11 | import java.util.Locale | 
| 49294 | 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 |   {
 | |
| 71381 | 30 | val r = java.lang.Integer.valueOf(c.getRed) | 
| 31 | val g = java.lang.Integer.valueOf(c.getGreen) | |
| 32 | val b = java.lang.Integer.valueOf(c.getBlue) | |
| 33 | val a = java.lang.Integer.valueOf(c.getAlpha) | |
| 62570 | 34 | Word.uppercase(String.format(Locale.ROOT, "%02x%02x%02x%02x", r, g, b, a)) | 
| 49294 | 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 | } |