--- a/src/Tools/Graphview/tree_panel.scala Sun Jan 18 22:22:12 2015 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Sun Jan 18 22:43:53 2015 +0100
@@ -106,7 +106,7 @@
private def selection_filter(node: Graph_Display.Node): Boolean =
selection_pattern match {
- case None => true
+ case None => false
case Some(re) => re.pattern.matcher(node.toString).find
}
@@ -130,8 +130,10 @@
}
if (selection_pattern != pattern) {
selection_pattern = pattern
- // FIXME
- System.console.writer.println(pattern)
+ tree.setSelectionRows(
+ (for { (node, i) <- nodes.iterator.zipWithIndex if selection_filter(node) }
+ yield i + 1).toArray)
+ tree.repaint()
}
selection_field.foreground =
if (ok) selection_field_foreground else visualizer.error_color