| 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 | 
 |