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