# HG changeset patch # User wenzelm # Date 1614803840 -3600 # Node ID 79b120d1c1a398359d60017b53a9d1b408f691a0 # Parent 279e45248e9d54577f72d834fdaacdb61f2f2d29 tuned --- fewer warnings; diff -r 279e45248e9d -r 79b120d1c1a3 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