# HG changeset patch
# User wenzelm
# Date 1579113964 -3600
# Node ID b9ea2467c929c48b189b0103e9c3cb3a67f708f8
# Parent  5965e6e3c3ece9329c37f3227e079762694e9e65
tuned -- avoid deprecated constructors;

diff -r 5965e6e3c3ec -r b9ea2467c929 src/Pure/GUI/color_value.scala
--- a/src/Pure/GUI/color_value.scala	Wed Jan 15 19:45:06 2020 +0100
+++ b/src/Pure/GUI/color_value.scala	Wed Jan 15 19:46:04 2020 +0100
@@ -27,10 +27,10 @@
 
   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)
+    val r = java.lang.Integer.valueOf(c.getRed)
+    val g = java.lang.Integer.valueOf(c.getGreen)
+    val b = java.lang.Integer.valueOf(c.getBlue)
+    val a = java.lang.Integer.valueOf(c.getAlpha)
     Word.uppercase(String.format(Locale.ROOT, "%02x%02x%02x%02x", r, g, b, a))
   }
 
diff -r 5965e6e3c3ec -r b9ea2467c929 src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Wed Jan 15 19:45:06 2020 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Wed Jan 15 19:46:04 2020 +0100
@@ -40,7 +40,7 @@
     font_style(style, font0 =>
       {
         val font1 =
-          font0.deriveFont(java.util.Map.of(TextAttribute.SUPERSCRIPT, new java.lang.Integer(i)))
+          font0.deriveFont(java.util.Map.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
 
         def shift(y: Float): Font =
           GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))