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