tuned --- fewer warnings;
authorwenzelm
Wed, 03 Mar 2021 21:37:20 +0100
changeset 73354 79b120d1c1a3
parent 73353 279e45248e9d
child 73355 ec52a1a6ed31
tuned --- fewer warnings;
src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Mar 03 21:19:36 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Mar 03 21:37:20 2021 +0100
@@ -15,6 +15,7 @@
 import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
 
 import scala.util.parsing.input.CharSequenceReader
+import scala.jdk.CollectionConverters._
 
 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
 import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
@@ -105,7 +106,8 @@
 
   /* main jEdit components */
 
-  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
+  def jedit_buffers(): Iterator[Buffer] =
+    jEdit.getBufferManager().getBuffers().asScala.iterator
 
   def jedit_buffer(name: String): Option[Buffer] =
     jedit_buffers().find(buffer => buffer_name(buffer) == name)
@@ -113,7 +115,8 @@
   def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
     jedit_buffer(name.node)
 
-  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
+  def jedit_views(): Iterator[View] =
+    jEdit.getViewManager().getViews().asScala.iterator
 
   def jedit_view(view: View = null): View =
     if (view == null) jEdit.getActiveView() else view