--- 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