src/Pure/GUI/color_value.scala

clarified mode of ROOT.ML files;

/*  Title:      Pure/GUI/color_value.scala
    Module:     PIDE-GUI
    Author:     Makarius

Cached color values.
*/

package isabelle


import java.awt.Color
import java.util.Locale


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)
    Word.uppercase(String.format(Locale.ROOT, "%02x%02x%02x%02x", r, g, b, a))
  }

  def apply(s: String): Color =
    synchronized {
      cache.get(s) match {
        case Some(c) => c
        case None =>
          val c = parse(s)
          cache += (s -> c)
          c
      }
    }
}