tuned -- avoid deprecated constructors;

--- a/src/Pure/Admin/build_log.scala	Mon Nov 25 12:16:26 2019 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Nov 25 12:19:14 2019 +0100
@@ -83,7 +83,7 @@
   def log_date(date: Date): String =
     String.format(Locale.ROOT, "%s.%05d",
       DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
-      new java.lang.Long((date.time - date.midnight.time).ms / 1000))
+      java.lang.Long.valueOf((date.time - date.midnight.time).ms / 1000))
 
   def log_subdir(date: Date): Path =
     Path.explode("log") + Path.explode(date.rep.getYear.toString)

--- a/src/Pure/General/time.scala	Mon Nov 25 12:16:26 2019 +0100
+++ b/src/Pure/General/time.scala	Mon Nov 25 12:19:14 2019 +0100
@@ -59,7 +59,9 @@
   {
     val s = ms / 1000
     String.format(Locale.ROOT, "%d:%02d:%02d",
-      new java.lang.Long(s / 3600), new java.lang.Long((s / 60) % 60), new java.lang.Long(s % 60))
+      java.lang.Long.valueOf(s / 3600),
+      java.lang.Long.valueOf((s / 60) % 60),
+      java.lang.Long.valueOf(s % 60))
   }
 
   def instant: Instant = Instant.ofEpochMilli(ms)

--- a/src/Pure/General/url.scala	Mon Nov 25 12:16:26 2019 +0100
+++ b/src/Pure/General/url.scala	Mon Nov 25 12:19:14 2019 +0100
@@ -19,7 +19,9 @@
   /* special characters */
 
   def escape_special(c: Char): String =
-    if ("!#$&'()*+,/:;=?@[]".contains(c)) String.format(Locale.ROOT, "%%%02X", new Integer(c.toInt))
+    if ("!#$&'()*+,/:;=?@[]".contains(c)) {
+      String.format(Locale.ROOT, "%%%02X", Integer.valueOf(c.toInt))
+    }
     else c.toString
 
   def escape_special(s: String): String = s.iterator.map(escape_special(_)).mkString

--- a/src/Pure/Tools/fontforge.scala	Mon Nov 25 12:16:26 2019 +0100
+++ b/src/Pure/Tools/fontforge.scala	Mon Nov 25 12:19:14 2019 +0100
@@ -24,7 +24,7 @@
   def string(s: String): Script =
   {
     def err(c: Char): Nothing =
-      error("Bad character \\u" + String.format(Locale.ROOT, "%04x", new Integer(c)) +
+      error("Bad character \\u" + String.format(Locale.ROOT, "%04x", Integer.valueOf(c)) +
         " in fontforge string " + quote(s))
 
     val q = if (s.contains('"')) '\'' else '"'

--- a/src/Tools/jEdit/src/fold_handling.scala	Mon Nov 25 12:16:26 2019 +0100
+++ b/src/Tools/jEdit/src/fold_handling.scala	Mon Nov 25 12:19:14 2019 +0100
@@ -43,7 +43,7 @@
         else Nil
 
       if (result.isEmpty) null
-      else WrapAsJava.seqAsJavaList(result.map(i => new Integer(i)))
+      else WrapAsJava.seqAsJavaList(result.map(Integer.valueOf))
     }
   }