more explicit iterator terminology, in accordance to Scala 2.8 library;
authorwenzelm
Wed Apr 02 20:22:12 2014 +0200 (2014-04-02)
changeset 56372fadb0fef09d7
parent 56371 fb9ae0727548
child 56373 0605d90be6fc
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;
src/Pure/General/graph.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/query_operation.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/build.scala
src/Pure/Tools/simplifier_trace.scala
src/Tools/Graphview/src/graph_panel.scala
src/Tools/Graphview/src/layout_pendulum.scala
src/Tools/Graphview/src/model.scala
src/Tools/Graphview/src/mutator.scala
src/Tools/Graphview/src/visualizer.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/General/graph.scala	Wed Apr 02 18:35:07 2014 +0200
     1.2 +++ b/src/Pure/General/graph.scala	Wed Apr 02 20:22:12 2014 +0200
     1.3 @@ -67,11 +67,13 @@
     1.4    def is_empty: Boolean = rep.isEmpty
     1.5    def defined(x: Key): Boolean = rep.isDefinedAt(x)
     1.6  
     1.7 -  def entries: Iterator[(Key, Entry)] = rep.iterator
     1.8 -  def keys: Iterator[Key] = entries.map(_._1)
     1.9 +  def iterator: Iterator[(Key, Entry)] = rep.iterator
    1.10 +
    1.11 +  def keys_iterator: Iterator[Key] = iterator.map(_._1)
    1.12 +  def keys: List[Key] = keys_iterator.toList
    1.13  
    1.14    def dest: List[((Key, A), List[Key])] =
    1.15 -    (for ((x, (i, (_, succs))) <- entries) yield ((x, i), succs.toList)).toList
    1.16 +    (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList
    1.17  
    1.18    override def toString: String =
    1.19      dest.map({ case ((x, _), ys) =>
    1.20 @@ -130,7 +132,7 @@
    1.21    /*strongly connected components; see: David King and John Launchbury,
    1.22      "Structuring Depth First Search Algorithms in Haskell"*/
    1.23    def strong_conn: List[List[Key]] =
    1.24 -    reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse
    1.25 +    reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse
    1.26  
    1.27  
    1.28    /* minimal and maximal elements */
    1.29 @@ -174,7 +176,7 @@
    1.30    }
    1.31  
    1.32    def restrict(pred: Key => Boolean): Graph[Key, A] =
    1.33 -    (this /: entries){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
    1.34 +    (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
    1.35  
    1.36  
    1.37    /* edge operations */
    1.38 @@ -232,17 +234,17 @@
    1.39      graph
    1.40    }
    1.41  
    1.42 -  def transitive_closure: Graph[Key, A] = (this /: keys)(_.transitive_step(_))
    1.43 +  def transitive_closure: Graph[Key, A] = (this /: keys_iterator)(_.transitive_step(_))
    1.44  
    1.45    def transitive_reduction_acyclic: Graph[Key, A] =
    1.46    {
    1.47      val trans = this.transitive_closure
    1.48 -    if (trans.entries.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
    1.49 +    if (trans.iterator.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
    1.50        error("Cyclic graph")
    1.51  
    1.52      var graph = this
    1.53      for {
    1.54 -      (x, (_, (_, succs))) <- this.entries
    1.55 +      (x, (_, (_, succs))) <- iterator
    1.56        y <- succs
    1.57        if trans.imm_preds(y).exists(z => trans.is_edge(x, z))
    1.58      } graph = graph.del_edge(x, y)
     2.1 --- a/src/Pure/PIDE/command.scala	Wed Apr 02 18:35:07 2014 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Wed Apr 02 20:22:12 2014 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4    {
     2.5      def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
     2.6      def get(serial: Long): Option[XML.Tree] = rep.get(serial)
     2.7 -    def entries: Iterator[Results.Entry] = rep.iterator
     2.8 +    def iterator: Iterator[Results.Entry] = rep.iterator
     2.9  
    2.10      def + (entry: Results.Entry): Results =
    2.11        if (defined(entry._1)) this
    2.12 @@ -44,7 +44,7 @@
    2.13      def ++ (other: Results): Results =
    2.14        if (this eq other) this
    2.15        else if (rep.isEmpty) other
    2.16 -      else (this /: other.entries)(_ + _)
    2.17 +      else (this /: other.iterator)(_ + _)
    2.18  
    2.19      override def hashCode: Int = rep.hashCode
    2.20      override def equals(that: Any): Boolean =
    2.21 @@ -52,7 +52,7 @@
    2.22          case other: Results => rep == other.rep
    2.23          case _ => false
    2.24        }
    2.25 -    override def toString: String = entries.mkString("Results(", ", ", ")")
    2.26 +    override def toString: String = iterator.mkString("Results(", ", ", ")")
    2.27    }
    2.28  
    2.29  
     3.1 --- a/src/Pure/PIDE/document.scala	Wed Apr 02 18:35:07 2014 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Wed Apr 02 20:22:12 2014 +0200
     3.3 @@ -274,7 +274,7 @@
     3.4    final class Nodes private(graph: Graph[Node.Name, Node])
     3.5    {
     3.6      def get_name(s: String): Option[Node.Name] =
     3.7 -      graph.keys.find(name => name.node == s)
     3.8 +      graph.keys_iterator.find(name => name.node == s)
     3.9  
    3.10      def apply(name: Node.Name): Node =
    3.11        graph.default_node(name, Node.empty).get_node(name)
    3.12 @@ -290,12 +290,12 @@
    3.13        new Nodes(graph3.map_node(name, _ => node))
    3.14      }
    3.15  
    3.16 -    def entries: Iterator[(Node.Name, Node)] =
    3.17 -      graph.entries.map({ case (name, (node, _)) => (name, node) })
    3.18 +    def iterator: Iterator[(Node.Name, Node)] =
    3.19 +      graph.iterator.map({ case (name, (node, _)) => (name, node) })
    3.20  
    3.21      def load_commands(file_name: Node.Name): List[Command] =
    3.22        (for {
    3.23 -        (_, node) <- entries
    3.24 +        (_, node) <- iterator
    3.25          cmd <- node.load_commands.iterator
    3.26          name <- cmd.blobs_names.iterator
    3.27          if name == file_name
    3.28 @@ -617,7 +617,7 @@
    3.29        for {
    3.30          (version_id, version) <- versions1.iterator
    3.31          command_execs = assignments1(version_id).command_execs
    3.32 -        (_, node) <- version.nodes.entries
    3.33 +        (_, node) <- version.nodes.iterator
    3.34          command <- node.commands.iterator
    3.35        } {
    3.36          for (digest <- command.blobs_digests; if !blobs1.contains(digest))
     4.1 --- a/src/Pure/PIDE/protocol.scala	Wed Apr 02 18:35:07 2014 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Apr 02 20:22:12 2014 +0200
     4.3 @@ -137,7 +137,7 @@
     4.4  
     4.5        if (status.is_running) running += 1
     4.6        else if (status.is_finished) {
     4.7 -        val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))
     4.8 +        val warning = states.exists(st => st.results.iterator.exists(p => is_warning(p._2)))
     4.9          if (warning) warned += 1 else finished += 1
    4.10        }
    4.11        else if (status.is_failed) failed += 1
     5.1 --- a/src/Pure/PIDE/query_operation.scala	Wed Apr 02 18:35:07 2014 +0200
     5.2 +++ b/src/Pure/PIDE/query_operation.scala	Wed Apr 02 20:22:12 2014 +0200
     5.3 @@ -83,7 +83,7 @@
     5.4  
     5.5      val results =
     5.6        (for {
     5.7 -        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.entries
     5.8 +        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
     5.9          if props.contains((Markup.INSTANCE, instance))
    5.10        } yield elem).toList
    5.11  
     6.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 18:35:07 2014 +0200
     6.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 20:22:12 2014 +0200
     6.3 @@ -182,7 +182,7 @@
     6.4      val (syntax, syntax_changed) =
     6.5        if (previous.is_init || updated_keywords) {
     6.6          val syntax =
     6.7 -          (base_syntax /: nodes.entries) {
     6.8 +          (base_syntax /: nodes.iterator) {
     6.9              case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
    6.10            }
    6.11          (syntax, true)
    6.12 @@ -449,7 +449,7 @@
    6.13        if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
    6.14        else {
    6.15          val reparse =
    6.16 -          (reparse0 /: nodes0.entries)({
    6.17 +          (reparse0 /: nodes0.iterator)({
    6.18              case (reparse, (name, node)) =>
    6.19                if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
    6.20                  name :: reparse
     7.1 --- a/src/Pure/Tools/build.scala	Wed Apr 02 18:35:07 2014 +0200
     7.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 02 20:22:12 2014 +0200
     7.3 @@ -122,7 +122,7 @@
     7.4              else graph.new_node(name, info)
     7.5          }
     7.6        val graph2 =
     7.7 -        (graph1 /: graph1.entries) {
     7.8 +        (graph1 /: graph1.iterator) {
     7.9            case (graph, (name, (info, _))) =>
    7.10              info.parent match {
    7.11                case None => graph
    7.12 @@ -159,12 +159,12 @@
    7.13  
    7.14        val pre_selected =
    7.15        {
    7.16 -        if (all_sessions) graph.keys.toList
    7.17 +        if (all_sessions) graph.keys
    7.18          else {
    7.19            val select_group = session_groups.toSet
    7.20            val select = sessions.toSet
    7.21            (for {
    7.22 -            (name, (info, _)) <- graph.entries
    7.23 +            (name, (info, _)) <- graph.iterator
    7.24              if info.select || select(name) || apply(name).groups.exists(select_group)
    7.25            } yield name).toList
    7.26          }
    7.27 @@ -180,7 +180,7 @@
    7.28      def topological_order: List[(String, Session_Info)] =
    7.29        graph.topological_order.map(name => (name, apply(name)))
    7.30  
    7.31 -    override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
    7.32 +    override def toString: String = graph.keys_iterator.mkString("Session_Tree(", ", ", ")")
    7.33    }
    7.34  
    7.35  
    7.36 @@ -323,7 +323,7 @@
    7.37      def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
    7.38      {
    7.39        val graph = tree.graph
    7.40 -      val sessions = graph.keys.toList
    7.41 +      val sessions = graph.keys
    7.42  
    7.43        val timings =
    7.44          sessions.par.map((name: String) =>
     8.1 --- a/src/Pure/Tools/simplifier_trace.scala	Wed Apr 02 18:35:07 2014 +0200
     8.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Wed Apr 02 20:22:12 2014 +0200
     8.3 @@ -184,7 +184,7 @@
     8.4            var new_context = contexts.getOrElse(id, Context())
     8.5            var new_serial = new_context.last_serial
     8.6  
     8.7 -          for ((serial, result) <- results.entries if serial > new_context.last_serial)
     8.8 +          for ((serial, result) <- results.iterator if serial > new_context.last_serial)
     8.9            {
    8.10              result match {
    8.11                case Item(markup, data) =>
    8.12 @@ -253,10 +253,10 @@
    8.13            // current results.
    8.14  
    8.15            val items =
    8.16 -            for { (_, Item(_, data)) <- results.entries }
    8.17 -              yield data
    8.18 +            (for { (_, Item(_, data)) <- results.iterator }
    8.19 +              yield data).toList
    8.20  
    8.21 -          reply(Trace(items.toList))
    8.22 +          reply(Trace(items))
    8.23  
    8.24          case Cancel(serial) =>
    8.25            find_question(serial) match {
     9.1 --- a/src/Tools/Graphview/src/graph_panel.scala	Wed Apr 02 18:35:07 2014 +0200
     9.2 +++ b/src/Tools/Graphview/src/graph_panel.scala	Wed Apr 02 20:22:12 2014 +0200
     9.3 @@ -47,7 +47,7 @@
     9.4    verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
     9.5  
     9.6    def node(at: Point2D): Option[String] =
     9.7 -    visualizer.model.visible_nodes()
     9.8 +    visualizer.model.visible_nodes_iterator
     9.9        .find(name => visualizer.Drawer.shape(visualizer.gfx, Some(name)).contains(at))
    9.10  
    9.11    def refresh()
    9.12 @@ -139,7 +139,7 @@
    9.13      }
    9.14  
    9.15      def fit_to_window() {
    9.16 -      if (visualizer.model.visible_nodes().isEmpty)
    9.17 +      if (visualizer.model.visible_nodes_iterator.isEmpty)
    9.18          rescale(1.0)
    9.19        else {
    9.20          val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
    9.21 @@ -197,7 +197,7 @@
    9.22        }
    9.23  
    9.24        def dummy(at: Point2D): Option[Dummy] =
    9.25 -        visualizer.model.visible_edges().map({
    9.26 +        visualizer.model.visible_edges_iterator.map({
    9.27              i => visualizer.Coordinates(i).zipWithIndex.map((i, _))
    9.28            }).flatten.find({
    9.29              case (_, ((x, y), _)) =>
    10.1 --- a/src/Tools/Graphview/src/layout_pendulum.scala	Wed Apr 02 18:35:07 2014 +0200
    10.2 +++ b/src/Tools/Graphview/src/layout_pendulum.scala	Wed Apr 02 20:22:12 2014 +0200
    10.3 @@ -32,7 +32,7 @@
    10.4        val initial_levels = level_map(graph)
    10.5  
    10.6        val (dummy_graph, dummies, dummy_levels) =
    10.7 -        ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys) {
    10.8 +        ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) {
    10.9            case ((graph, dummies, levels), from) =>
   10.10              ((graph, dummies, levels) /: graph.imm_succs(from)) {
   10.11                case ((graph, dummies, levels), to) =>
    11.1 --- a/src/Tools/Graphview/src/model.scala	Wed Apr 02 18:35:07 2014 +0200
    11.2 +++ b/src/Tools/Graphview/src/model.scala	Wed Apr 02 20:22:12 2014 +0200
    11.3 @@ -75,10 +75,10 @@
    11.4        Node_List(Nil, false, false, false)
    11.5      ))  
    11.6    
    11.7 -  def visible_nodes(): Iterator[String] = current.keys
    11.8 +  def visible_nodes_iterator: Iterator[String] = current.keys_iterator
    11.9    
   11.10 -  def visible_edges(): Iterator[(String, String)] =
   11.11 -    current.keys.map(k => current.imm_succs(k).map((k, _))).flatten  // FIXME iterator
   11.12 +  def visible_edges_iterator: Iterator[(String, String)] =
   11.13 +    current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _)))
   11.14    
   11.15    def complete = graph
   11.16    def current: Model.Graph =
   11.17 @@ -96,7 +96,7 @@
   11.18      _colors = 
   11.19        (Map.empty[String, Color] /: Colors()) ({
   11.20            case (colors, (enabled, color, mutator)) => {
   11.21 -              (colors /: mutator.mutate(graph, graph).keys) ({
   11.22 +              (colors /: mutator.mutate(graph, graph).keys_iterator) ({
   11.23                    case (colors, k) => colors + (k -> color)
   11.24                  })
   11.25              }
    12.1 --- a/src/Tools/Graphview/src/mutator.scala	Wed Apr 02 18:35:07 2014 +0200
    12.2 +++ b/src/Tools/Graphview/src/mutator.scala	Wed Apr 02 20:22:12 2014 +0200
    12.3 @@ -148,7 +148,7 @@
    12.4          def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) =
    12.5            (g /: keys) {
    12.6              (graph, end) => {
    12.7 -              if (!graph.keys.contains(end)) graph
    12.8 +              if (!graph.keys_iterator.contains(end)) graph
    12.9                else {
   12.10                  if (succs) graph.add_edge(key, end)
   12.11                  else graph.add_edge(end, key)
   12.12 @@ -186,13 +186,12 @@
   12.13      (complete, sub) => {     
   12.14        val withparents = 
   12.15          if (parents)
   12.16 -          add_node_group(complete, sub, complete.all_preds(sub.keys.toList))
   12.17 +          add_node_group(complete, sub, complete.all_preds(sub.keys))
   12.18          else
   12.19            sub
   12.20        
   12.21        if (children)
   12.22 -        add_node_group(complete, withparents,
   12.23 -                       complete.all_succs(sub.keys.toList))
   12.24 +        add_node_group(complete, withparents, complete.all_succs(sub.keys))
   12.25        else 
   12.26          withparents
   12.27      }
    13.1 --- a/src/Tools/Graphview/src/visualizer.scala	Wed Apr 02 18:35:07 2014 +0200
    13.2 +++ b/src/Tools/Graphview/src/visualizer.scala	Wed Apr 02 20:22:12 2014 +0200
    13.3 @@ -122,7 +122,7 @@
    13.4          if (model.current.is_empty) Layout_Pendulum.empty_layout
    13.5          else {
    13.6            val max_width =
    13.7 -            model.current.entries.map({ case (_, (info, _)) =>
    13.8 +            model.current.iterator.map({ case (_, (info, _)) =>
    13.9                font_metrics.stringWidth(info.name).toDouble }).max
   13.10            val box_distance = max_width + pad_x + gap_x
   13.11            def box_height(n: Int): Double =
   13.12 @@ -132,7 +132,7 @@
   13.13      }
   13.14  
   13.15      def bounds(): (Double, Double, Double, Double) =
   13.16 -      model.visible_nodes().toList match {
   13.17 +      model.visible_nodes_iterator.toList match {
   13.18          case Nil => (0, 0, 0, 0)
   13.19          case nodes =>
   13.20            val X: (String => Double) = (n => apply(n)._1)
   13.21 @@ -164,11 +164,11 @@
   13.22  
   13.23        g.setRenderingHints(rendering_hints)
   13.24  
   13.25 -      model.visible_edges().foreach(e => {
   13.26 +      model.visible_edges_iterator.foreach(e => {
   13.27            apply(g, e, arrow_heads, dummies)
   13.28          })
   13.29  
   13.30 -      model.visible_nodes().foreach(l => {
   13.31 +      model.visible_nodes_iterator.foreach(l => {
   13.32            apply(g, Some(l))
   13.33          })
   13.34      }
    14.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Apr 02 18:35:07 2014 +0200
    14.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Apr 02 20:22:12 2014 +0200
    14.3 @@ -426,7 +426,7 @@
    14.4      else {
    14.5        val r = Text.Range(results.head.range.start, results.last.range.stop)
    14.6        val msgs = Command.Results.make(results.map(_.info))
    14.7 -      Some(Text.Info(r, Pretty.separate(msgs.entries.map(_._2).toList)))
    14.8 +      Some(Text.Info(r, Pretty.separate(msgs.iterator.map(_._2).toList)))
    14.9      }
   14.10    }
   14.11  
   14.12 @@ -590,7 +590,7 @@
   14.13    }
   14.14  
   14.15    def output_messages(results: Command.Results): List[XML.Tree] =
   14.16 -    results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
   14.17 +    results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
   14.18  
   14.19  
   14.20    /* text background */
    15.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Apr 02 18:35:07 2014 +0200
    15.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Apr 02 20:22:12 2014 +0200
    15.3 @@ -188,7 +188,7 @@
    15.4      val iterator =
    15.5        (restriction match {
    15.6          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
    15.7 -        case None => snapshot.version.nodes.entries
    15.8 +        case None => snapshot.version.nodes.iterator
    15.9        }).filter(_._1.is_theory)
   15.10      val nodes_status1 =
   15.11        (nodes_status /: iterator)({ case (status, (name, node)) =>
    16.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Apr 02 18:35:07 2014 +0200
    16.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Apr 02 20:22:12 2014 +0200
    16.3 @@ -182,7 +182,7 @@
    16.4      val iterator =
    16.5        restriction match {
    16.6          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
    16.7 -        case None => snapshot.version.nodes.entries
    16.8 +        case None => snapshot.version.nodes.iterator
    16.9        }
   16.10      val nodes_timing1 =
   16.11        (nodes_timing /: iterator)({ case (timing1, (name, node)) =>