diff -r afcccb9bfa3b -r a600c017f814 src/Pure/System/color_value.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/color_value.scala	Tue Sep 11 22:54:12 2012 +0200
@@ -0,0 +1,48 @@
+/*  Title:      Pure/General/color_value.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Cached color values.
+*/
+
+package isabelle
+
+
+import java.awt.Color
+
+
+object Color_Value
+{
+  private var cache = Map.empty[String, Color]
+
+  def parse(s: String): Color =
+  {
+    val i = java.lang.Long.parseLong(s, 16)
+    val r = ((i >> 24) & 0xFF).toInt
+    val g = ((i >> 16) & 0xFF).toInt
+    val b = ((i >> 8) & 0xFF).toInt
+    val a = (i & 0xFF).toInt
+    new Color(r, g, b, a)
+  }
+
+  def print(c: Color): String =
+  {
+    val r = new java.lang.Integer(c.getRed)
+    val g = new java.lang.Integer(c.getGreen)
+    val b = new java.lang.Integer(c.getBlue)
+    val a = new java.lang.Integer(c.getAlpha)
+    String.format("%02x%02x%02x%02x", r, g, b, a).toUpperCase
+  }
+
+  def apply(s: String): Color =
+    synchronized {
+      cache.get(s) match {
+        case Some(c) => c
+        case None =>
+          val c = parse(s)
+          cache += (s -> c)
+          c
+      }
+    }
+}
+