# HG changeset patch
# User wenzelm
# Date 1614884152 -3600
# Node ID 5f388e514ab800c6c674d406f4060d7138fc0cb2
# Parent  a78b5ffc0f463e14e98c5b0d54e648ff345e40bb
tuned --- fewer warnings;

diff -r a78b5ffc0f46 -r 5f388e514ab8 src/Pure/System/isabelle_charset.scala
--- a/src/Pure/System/isabelle_charset.scala	Thu Mar 04 18:04:16 2021 +0100
+++ b/src/Pure/System/isabelle_charset.scala	Thu Mar 04 19:55:52 2021 +0100
@@ -12,8 +12,6 @@
 import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
 import java.nio.charset.spi.CharsetProvider
 
-import scala.collection.JavaConverters
-
 
 object Isabelle_Charset
 {
@@ -47,6 +45,6 @@
   {
     // FIXME inactive
     // Iterator(Isabelle_Charset.charset)
-    JavaConverters.asJavaIterator(Iterator())
+    java.util.List.of[Charset]().listIterator()
   }
 }