avoid deprecated Iterator.fromArray;
authorwenzelm
Fri May 28 21:40:32 2010 +0200 (2010-05-28)
changeset 3717717331ca75044
parent 37176 6f3c9ed34689
child 37178 d52f934f8ff6
avoid deprecated Iterator.fromArray;
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri May 28 21:37:24 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri May 28 21:40:32 2010 +0200
     1.3 @@ -104,12 +104,12 @@
     1.4  
     1.5    /* main jEdit components */  // FIXME ownership!?
     1.6  
     1.7 -  def jedit_buffers(): Iterator[Buffer] = Iterator.fromArray(jEdit.getBuffers())
     1.8 +  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
     1.9  
    1.10 -  def jedit_views(): Iterator[View] = Iterator.fromArray(jEdit.getViews())
    1.11 +  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    1.12  
    1.13    def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    1.14 -    Iterator.fromArray(view.getEditPanes).map(_.getTextArea)
    1.15 +    view.getEditPanes().iterator.map(_.getTextArea)
    1.16  
    1.17    def jedit_text_areas(): Iterator[JEditTextArea] =
    1.18      jedit_views().flatMap(jedit_text_areas(_))