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;
--- 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)
--- 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(", ", ", ")")
}
--- 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))
--- 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
--- 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
--- 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
--- 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) =>
--- 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 {
--- 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), _)) =>
--- 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) =>
--- 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)
})
}
--- 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
}
--- 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))
})
}
--- 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 */
--- 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)) =>
--- 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)) =>