# HG changeset patch
# User wenzelm
# Date 1397236076 -7200
# Node ID 902960859c66431a0cea3974cd948e1a3b9afabf
# Parent  1fd920a86173ff0ee473602159f098893bba84bf
prefere standard Isabelle/Scala operation, with fixed locale;

diff -r 1fd920a86173 -r 902960859c66 src/Pure/GUI/color_value.scala
--- a/src/Pure/GUI/color_value.scala	Fri Apr 11 17:53:16 2014 +0200
+++ b/src/Pure/GUI/color_value.scala	Fri Apr 11 19:07:56 2014 +0200
@@ -31,7 +31,7 @@
     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
+    Library.uppercase(String.format("%02x%02x%02x%02x", r, g, b, a))
   }
 
   def apply(s: String): Color =