src/Tools/jEdit/src/jedit_lib.scala
changeset 73354 79b120d1c1a3
parent 73340 0ffcad1f6130
child 73367 77ef8bef0593
equal deleted inserted replaced
73353:279e45248e9d 73354:79b120d1c1a3
    13 import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit}
    13 import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit}
    14 import java.awt.event.{InputEvent, KeyEvent, KeyListener}
    14 import java.awt.event.{InputEvent, KeyEvent, KeyListener}
    15 import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
    15 import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
    16 
    16 
    17 import scala.util.parsing.input.CharSequenceReader
    17 import scala.util.parsing.input.CharSequenceReader
       
    18 import scala.jdk.CollectionConverters._
    18 
    19 
    19 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
    20 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
    20 import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
    21 import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
    21 import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}
    22 import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}
    22 import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
    23 import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
   103   }
   104   }
   104 
   105 
   105 
   106 
   106   /* main jEdit components */
   107   /* main jEdit components */
   107 
   108 
   108   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
   109   def jedit_buffers(): Iterator[Buffer] =
       
   110     jEdit.getBufferManager().getBuffers().asScala.iterator
   109 
   111 
   110   def jedit_buffer(name: String): Option[Buffer] =
   112   def jedit_buffer(name: String): Option[Buffer] =
   111     jedit_buffers().find(buffer => buffer_name(buffer) == name)
   113     jedit_buffers().find(buffer => buffer_name(buffer) == name)
   112 
   114 
   113   def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
   115   def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
   114     jedit_buffer(name.node)
   116     jedit_buffer(name.node)
   115 
   117 
   116   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
   118   def jedit_views(): Iterator[View] =
       
   119     jEdit.getViewManager().getViews().asScala.iterator
   117 
   120 
   118   def jedit_view(view: View = null): View =
   121   def jedit_view(view: View = null): View =
   119     if (view == null) jEdit.getActiveView() else view
   122     if (view == null) jEdit.getActiveView() else view
   120 
   123 
   121   def jedit_edit_panes(view: View): Iterator[EditPane] =
   124   def jedit_edit_panes(view: View): Iterator[EditPane] =