src/Pure/System/color_value.scala
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 49322 fbb320d02420
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
     1 /*  Title:      Pure/System/color_value.scala
     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