src/Pure/GUI/color_value.scala
changeset 71381 b9ea2467c929
parent 70083 96776eb41854
child 75393 87ebf5a50283
equal deleted inserted replaced
71380:5965e6e3c3ec 71381:b9ea2467c929
    25     new Color(r, g, b, a)
    25     new Color(r, g, b, a)
    26   }
    26   }
    27 
    27 
    28   def print(c: Color): String =
    28   def print(c: Color): String =
    29   {
    29   {
    30     val r = new java.lang.Integer(c.getRed)
    30     val r = java.lang.Integer.valueOf(c.getRed)
    31     val g = new java.lang.Integer(c.getGreen)
    31     val g = java.lang.Integer.valueOf(c.getGreen)
    32     val b = new java.lang.Integer(c.getBlue)
    32     val b = java.lang.Integer.valueOf(c.getBlue)
    33     val a = new java.lang.Integer(c.getAlpha)
    33     val a = java.lang.Integer.valueOf(c.getAlpha)
    34     Word.uppercase(String.format(Locale.ROOT, "%02x%02x%02x%02x", r, g, b, a))
    34     Word.uppercase(String.format(Locale.ROOT, "%02x%02x%02x%02x", r, g, b, a))
    35   }
    35   }
    36 
    36 
    37   def apply(s: String): Color =
    37   def apply(s: String): Color =
    38     synchronized {
    38     synchronized {