avoid deprecated Iterator.fromArray;
authorwenzelm
Fri, 28 May 2010 21:40:32 +0200
changeset 37177 17331ca75044
parent 37176 6f3c9ed34689
child 37178 d52f934f8ff6
avoid deprecated Iterator.fromArray;
src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri May 28 21:37:24 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri May 28 21:40:32 2010 +0200
@@ -104,12 +104,12 @@
 
   /* main jEdit components */  // FIXME ownership!?
 
-  def jedit_buffers(): Iterator[Buffer] = Iterator.fromArray(jEdit.getBuffers())
+  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
 
-  def jedit_views(): Iterator[View] = Iterator.fromArray(jEdit.getViews())
+  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
 
   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
-    Iterator.fromArray(view.getEditPanes).map(_.getTextArea)
+    view.getEditPanes().iterator.map(_.getTextArea)
 
   def jedit_text_areas(): Iterator[JEditTextArea] =
     jedit_views().flatMap(jedit_text_areas(_))