# HG changeset patch
# User wenzelm
# Date 1421617433 -3600
# Node ID 4de91de47a6cee91dafa2ce61bf6a1ccbdb962ee
# Parent  6ee01e0119768ec84abd4fcee7aba05a48ab211c
proper selection of nodes via regular expression;

diff -r 6ee01e011976 -r 4de91de47a6c src/Tools/Graphview/tree_panel.scala
--- 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