# HG changeset patch # User wenzelm # Date 1574680754 -3600 # Node ID b5822f4c3fdecc0c6d34db287d29dbd812ce019e # Parent 4b3e1b859a2220551762c2a61c7f94744574d891 tuned -- avoid deprecated constructors; diff -r 4b3e1b859a22 -r b5822f4c3fde src/Pure/Admin/build_log.scala --- 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) diff -r 4b3e1b859a22 -r b5822f4c3fde src/Pure/General/time.scala --- 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) diff -r 4b3e1b859a22 -r b5822f4c3fde src/Pure/General/url.scala --- 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 diff -r 4b3e1b859a22 -r b5822f4c3fde src/Pure/Tools/fontforge.scala --- 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 '"' diff -r 4b3e1b859a22 -r b5822f4c3fde src/Tools/jEdit/src/fold_handling.scala --- 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)) } }