# HG changeset patch
# User wenzelm
# Date 1396386262 -7200
# Node ID c3dbaa155ece8ac0503c7536c4b45cecfc39e033
# Parent  1a9f569b5b7e16760fc419df8f17e7216be795c7
tuned for-comprehensions -- less structure mapping;

diff -r 1a9f569b5b7e -r c3dbaa155ece src/Pure/GUI/wrap_panel.scala
--- a/src/Pure/GUI/wrap_panel.scala	Tue Apr 01 22:25:01 2014 +0200
+++ b/src/Pure/GUI/wrap_panel.scala	Tue Apr 01 23:04:22 2014 +0200
@@ -62,7 +62,7 @@
         }
 
         for {
-          i <- 0 until target.getComponentCount
+          i <- (0 until target.getComponentCount).iterator
           m = target.getComponent(i)
           if m.isVisible
           d = if (preferred) m.getPreferredSize else m.getMinimumSize()
diff -r 1a9f569b5b7e -r c3dbaa155ece src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Apr 01 22:25:01 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Apr 01 23:04:22 2014 +0200
@@ -61,8 +61,8 @@
     var failed = false
     var forks = 0
     var runs = 0
-    for { markup <- markups; name = markup.name }
-      name match {
+    for (markup <- markups) {
+      markup.name match {
         case Markup.ACCEPTED => accepted = true
         case Markup.FORKED => touched = true; forks += 1
         case Markup.JOINED => forks -= 1
@@ -71,6 +71,7 @@
         case Markup.FAILED => failed = true
         case _ =>
       }
+    }
     Status(touched, accepted, failed, forks, runs)
   }
 
@@ -114,8 +115,7 @@
     var finished = 0
     var warned = 0
     var failed = 0
-    for { command <- node.commands }
-    {
+    for (command <- node.commands.iterator) {
       val states = state.command_states(version, command)
       val status = command_status(states.iterator.flatMap(st => st.status.iterator))
 
@@ -148,12 +148,12 @@
     for {
       command <- node.commands.iterator
       st <- state.command_states(version, command)
-      command_timing =
+    } {
+      val command_timing =
         (0.0 /: st.status)({
           case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
           case (timing, _) => timing
         })
-    } {
       total += command_timing
       if (command_timing >= threshold) commands += (command -> command_timing)
     }
diff -r 1a9f569b5b7e -r c3dbaa155ece src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 01 22:25:01 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 01 23:04:22 2014 +0200
@@ -94,7 +94,7 @@
     val buffer_range = JEdit_Lib.buffer_range(model.buffer)
     val visible_lines =
       (for {
-        i <- 0 until text_area.getVisibleLines
+        i <- (0 until text_area.getVisibleLines).iterator
         start = text_area.getScreenLineStartOffset(i)
         stop = text_area.getScreenLineEndOffset(i)
         if start >= 0 && stop >= 0
@@ -228,7 +228,7 @@
                       snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
                     if (visible_cmds.exists(changed.commands)) {
                       for {
-                        line <- 0 until visible_lines
+                        line <- (0 until visible_lines).iterator
                         start = text_area.getScreenLineStartOffset(line) if start >= 0
                         end = text_area.getScreenLineEndOffset(line) if end >= 0
                         range = Text.Range(start, end)