# HG changeset patch
# User wenzelm
# Date 1275075632 -7200
# Node ID 17331ca7504481caf16b5fba414c16c0e3abf106
# Parent  6f3c9ed34689f980b94b545e174133469ef386e6
avoid deprecated Iterator.fromArray;

diff -r 6f3c9ed34689 -r 17331ca75044 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(_))