# HG changeset patch
# User wenzelm
# Date 1396462932 -7200
# Node ID fadb0fef09d789c32922058cf2a87e0ca997e4d2
# Parent  fb9ae0727548bea146b9bb224d17f9386e48e348
more explicit iterator terminology, in accordance to Scala 2.8 library;
clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics;
tuned output;

diff -r fb9ae0727548 -r fadb0fef09d7 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Pure/General/graph.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -67,11 +67,13 @@
   def is_empty: Boolean = rep.isEmpty
   def defined(x: Key): Boolean = rep.isDefinedAt(x)
 
-  def entries: Iterator[(Key, Entry)] = rep.iterator
-  def keys: Iterator[Key] = entries.map(_._1)
+  def iterator: Iterator[(Key, Entry)] = rep.iterator
+
+  def keys_iterator: Iterator[Key] = iterator.map(_._1)
+  def keys: List[Key] = keys_iterator.toList
 
   def dest: List[((Key, A), List[Key])] =
-    (for ((x, (i, (_, succs))) <- entries) yield ((x, i), succs.toList)).toList
+    (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList
 
   override def toString: String =
     dest.map({ case ((x, _), ys) =>
@@ -130,7 +132,7 @@
   /*strongly connected components; see: David King and John Launchbury,
     "Structuring Depth First Search Algorithms in Haskell"*/
   def strong_conn: List[List[Key]] =
-    reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse
+    reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse
 
 
   /* minimal and maximal elements */
@@ -174,7 +176,7 @@
   }
 
   def restrict(pred: Key => Boolean): Graph[Key, A] =
-    (this /: entries){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
+    (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
 
 
   /* edge operations */
@@ -232,17 +234,17 @@
     graph
   }
 
-  def transitive_closure: Graph[Key, A] = (this /: keys)(_.transitive_step(_))
+  def transitive_closure: Graph[Key, A] = (this /: keys_iterator)(_.transitive_step(_))
 
   def transitive_reduction_acyclic: Graph[Key, A] =
   {
     val trans = this.transitive_closure
-    if (trans.entries.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
+    if (trans.iterator.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
       error("Cyclic graph")
 
     var graph = this
     for {
-      (x, (_, (_, succs))) <- this.entries
+      (x, (_, (_, succs))) <- iterator
       y <- succs
       if trans.imm_preds(y).exists(z => trans.is_edge(x, z))
     } graph = graph.del_edge(x, y)
diff -r fb9ae0727548 -r fadb0fef09d7 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -35,7 +35,7 @@
   {
     def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
     def get(serial: Long): Option[XML.Tree] = rep.get(serial)
-    def entries: Iterator[Results.Entry] = rep.iterator
+    def iterator: Iterator[Results.Entry] = rep.iterator
 
     def + (entry: Results.Entry): Results =
       if (defined(entry._1)) this
@@ -44,7 +44,7 @@
     def ++ (other: Results): Results =
       if (this eq other) this
       else if (rep.isEmpty) other
-      else (this /: other.entries)(_ + _)
+      else (this /: other.iterator)(_ + _)
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
@@ -52,7 +52,7 @@
         case other: Results => rep == other.rep
         case _ => false
       }
-    override def toString: String = entries.mkString("Results(", ", ", ")")
+    override def toString: String = iterator.mkString("Results(", ", ", ")")
   }
 
 
diff -r fb9ae0727548 -r fadb0fef09d7 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -274,7 +274,7 @@
   final class Nodes private(graph: Graph[Node.Name, Node])
   {
     def get_name(s: String): Option[Node.Name] =
-      graph.keys.find(name => name.node == s)
+      graph.keys_iterator.find(name => name.node == s)
 
     def apply(name: Node.Name): Node =
       graph.default_node(name, Node.empty).get_node(name)
@@ -290,12 +290,12 @@
       new Nodes(graph3.map_node(name, _ => node))
     }
 
-    def entries: Iterator[(Node.Name, Node)] =
-      graph.entries.map({ case (name, (node, _)) => (name, node) })
+    def iterator: Iterator[(Node.Name, Node)] =
+      graph.iterator.map({ case (name, (node, _)) => (name, node) })
 
     def load_commands(file_name: Node.Name): List[Command] =
       (for {
-        (_, node) <- entries
+        (_, node) <- iterator
         cmd <- node.load_commands.iterator
         name <- cmd.blobs_names.iterator
         if name == file_name
@@ -617,7 +617,7 @@
       for {
         (version_id, version) <- versions1.iterator
         command_execs = assignments1(version_id).command_execs
-        (_, node) <- version.nodes.entries
+        (_, node) <- version.nodes.iterator
         command <- node.commands.iterator
       } {
         for (digest <- command.blobs_digests; if !blobs1.contains(digest))
diff -r fb9ae0727548 -r fadb0fef09d7 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -137,7 +137,7 @@
 
       if (status.is_running) running += 1
       else if (status.is_finished) {
-        val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))
+        val warning = states.exists(st => st.results.iterator.exists(p => is_warning(p._2)))
         if (warning) warned += 1 else finished += 1
       }
       else if (status.is_failed) failed += 1
diff -r fb9ae0727548 -r fadb0fef09d7 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -83,7 +83,7 @@
 
     val results =
       (for {
-        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.entries
+        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
         if props.contains((Markup.INSTANCE, instance))
       } yield elem).toList
 
diff -r fb9ae0727548 -r fadb0fef09d7 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -182,7 +182,7 @@
     val (syntax, syntax_changed) =
       if (previous.is_init || updated_keywords) {
         val syntax =
-          (base_syntax /: nodes.entries) {
+          (base_syntax /: nodes.iterator) {
             case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
           }
         (syntax, true)
@@ -449,7 +449,7 @@
       if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
       else {
         val reparse =
-          (reparse0 /: nodes0.entries)({
+          (reparse0 /: nodes0.iterator)({
             case (reparse, (name, node)) =>
               if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
                 name :: reparse
diff -r fb9ae0727548 -r fadb0fef09d7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -122,7 +122,7 @@
             else graph.new_node(name, info)
         }
       val graph2 =
-        (graph1 /: graph1.entries) {
+        (graph1 /: graph1.iterator) {
           case (graph, (name, (info, _))) =>
             info.parent match {
               case None => graph
@@ -159,12 +159,12 @@
 
       val pre_selected =
       {
-        if (all_sessions) graph.keys.toList
+        if (all_sessions) graph.keys
         else {
           val select_group = session_groups.toSet
           val select = sessions.toSet
           (for {
-            (name, (info, _)) <- graph.entries
+            (name, (info, _)) <- graph.iterator
             if info.select || select(name) || apply(name).groups.exists(select_group)
           } yield name).toList
         }
@@ -180,7 +180,7 @@
     def topological_order: List[(String, Session_Info)] =
       graph.topological_order.map(name => (name, apply(name)))
 
-    override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
+    override def toString: String = graph.keys_iterator.mkString("Session_Tree(", ", ", ")")
   }
 
 
@@ -323,7 +323,7 @@
     def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
     {
       val graph = tree.graph
-      val sessions = graph.keys.toList
+      val sessions = graph.keys
 
       val timings =
         sessions.par.map((name: String) =>
diff -r fb9ae0727548 -r fadb0fef09d7 src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -184,7 +184,7 @@
           var new_context = contexts.getOrElse(id, Context())
           var new_serial = new_context.last_serial
 
-          for ((serial, result) <- results.entries if serial > new_context.last_serial)
+          for ((serial, result) <- results.iterator if serial > new_context.last_serial)
           {
             result match {
               case Item(markup, data) =>
@@ -253,10 +253,10 @@
           // current results.
 
           val items =
-            for { (_, Item(_, data)) <- results.entries }
-              yield data
+            (for { (_, Item(_, data)) <- results.iterator }
+              yield data).toList
 
-          reply(Trace(items.toList))
+          reply(Trace(items))
 
         case Cancel(serial) =>
           find_question(serial) match {
diff -r fb9ae0727548 -r fadb0fef09d7 src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -47,7 +47,7 @@
   verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
 
   def node(at: Point2D): Option[String] =
-    visualizer.model.visible_nodes()
+    visualizer.model.visible_nodes_iterator
       .find(name => visualizer.Drawer.shape(visualizer.gfx, Some(name)).contains(at))
 
   def refresh()
@@ -139,7 +139,7 @@
     }
 
     def fit_to_window() {
-      if (visualizer.model.visible_nodes().isEmpty)
+      if (visualizer.model.visible_nodes_iterator.isEmpty)
         rescale(1.0)
       else {
         val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
@@ -197,7 +197,7 @@
       }
 
       def dummy(at: Point2D): Option[Dummy] =
-        visualizer.model.visible_edges().map({
+        visualizer.model.visible_edges_iterator.map({
             i => visualizer.Coordinates(i).zipWithIndex.map((i, _))
           }).flatten.find({
             case (_, ((x, y), _)) =>
diff -r fb9ae0727548 -r fadb0fef09d7 src/Tools/Graphview/src/layout_pendulum.scala
--- a/src/Tools/Graphview/src/layout_pendulum.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/Graphview/src/layout_pendulum.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -32,7 +32,7 @@
       val initial_levels = level_map(graph)
 
       val (dummy_graph, dummies, dummy_levels) =
-        ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys) {
+        ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) {
           case ((graph, dummies, levels), from) =>
             ((graph, dummies, levels) /: graph.imm_succs(from)) {
               case ((graph, dummies, levels), to) =>
diff -r fb9ae0727548 -r fadb0fef09d7 src/Tools/Graphview/src/model.scala
--- a/src/Tools/Graphview/src/model.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/Graphview/src/model.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -75,10 +75,10 @@
       Node_List(Nil, false, false, false)
     ))  
   
-  def visible_nodes(): Iterator[String] = current.keys
+  def visible_nodes_iterator: Iterator[String] = current.keys_iterator
   
-  def visible_edges(): Iterator[(String, String)] =
-    current.keys.map(k => current.imm_succs(k).map((k, _))).flatten  // FIXME iterator
+  def visible_edges_iterator: Iterator[(String, String)] =
+    current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _)))
   
   def complete = graph
   def current: Model.Graph =
@@ -96,7 +96,7 @@
     _colors = 
       (Map.empty[String, Color] /: Colors()) ({
           case (colors, (enabled, color, mutator)) => {
-              (colors /: mutator.mutate(graph, graph).keys) ({
+              (colors /: mutator.mutate(graph, graph).keys_iterator) ({
                   case (colors, k) => colors + (k -> color)
                 })
             }
diff -r fb9ae0727548 -r fadb0fef09d7 src/Tools/Graphview/src/mutator.scala
--- a/src/Tools/Graphview/src/mutator.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/Graphview/src/mutator.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -148,7 +148,7 @@
         def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) =
           (g /: keys) {
             (graph, end) => {
-              if (!graph.keys.contains(end)) graph
+              if (!graph.keys_iterator.contains(end)) graph
               else {
                 if (succs) graph.add_edge(key, end)
                 else graph.add_edge(end, key)
@@ -186,13 +186,12 @@
     (complete, sub) => {     
       val withparents = 
         if (parents)
-          add_node_group(complete, sub, complete.all_preds(sub.keys.toList))
+          add_node_group(complete, sub, complete.all_preds(sub.keys))
         else
           sub
       
       if (children)
-        add_node_group(complete, withparents,
-                       complete.all_succs(sub.keys.toList))
+        add_node_group(complete, withparents, complete.all_succs(sub.keys))
       else 
         withparents
     }
diff -r fb9ae0727548 -r fadb0fef09d7 src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/Graphview/src/visualizer.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -122,7 +122,7 @@
         if (model.current.is_empty) Layout_Pendulum.empty_layout
         else {
           val max_width =
-            model.current.entries.map({ case (_, (info, _)) =>
+            model.current.iterator.map({ case (_, (info, _)) =>
               font_metrics.stringWidth(info.name).toDouble }).max
           val box_distance = max_width + pad_x + gap_x
           def box_height(n: Int): Double =
@@ -132,7 +132,7 @@
     }
 
     def bounds(): (Double, Double, Double, Double) =
-      model.visible_nodes().toList match {
+      model.visible_nodes_iterator.toList match {
         case Nil => (0, 0, 0, 0)
         case nodes =>
           val X: (String => Double) = (n => apply(n)._1)
@@ -164,11 +164,11 @@
 
       g.setRenderingHints(rendering_hints)
 
-      model.visible_edges().foreach(e => {
+      model.visible_edges_iterator.foreach(e => {
           apply(g, e, arrow_heads, dummies)
         })
 
-      model.visible_nodes().foreach(l => {
+      model.visible_nodes_iterator.foreach(l => {
           apply(g, Some(l))
         })
     }
diff -r fb9ae0727548 -r fadb0fef09d7 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -426,7 +426,7 @@
     else {
       val r = Text.Range(results.head.range.start, results.last.range.stop)
       val msgs = Command.Results.make(results.map(_.info))
-      Some(Text.Info(r, Pretty.separate(msgs.entries.map(_._2).toList)))
+      Some(Text.Info(r, Pretty.separate(msgs.iterator.map(_._2).toList)))
     }
   }
 
@@ -590,7 +590,7 @@
   }
 
   def output_messages(results: Command.Results): List[XML.Tree] =
-    results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
+    results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
 
 
   /* text background */
diff -r fb9ae0727548 -r fadb0fef09d7 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -188,7 +188,7 @@
     val iterator =
       (restriction match {
         case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
-        case None => snapshot.version.nodes.entries
+        case None => snapshot.version.nodes.iterator
       }).filter(_._1.is_theory)
     val nodes_status1 =
       (nodes_status /: iterator)({ case (status, (name, node)) =>
diff -r fb9ae0727548 -r fadb0fef09d7 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Apr 02 18:35:07 2014 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Apr 02 20:22:12 2014 +0200
@@ -182,7 +182,7 @@
     val iterator =
       restriction match {
         case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
-        case None => snapshot.version.nodes.entries
+        case None => snapshot.version.nodes.iterator
       }
     val nodes_timing1 =
       (nodes_timing /: iterator)({ case (timing1, (name, node)) =>