# HG changeset patch
# User wenzelm
# Date 1421616048 -3600
# Node ID d833cba5cce5309fc6098c6b6efa922b0269b67a
# Parent  47fb85ccfce8f0d42c5b4aaf484d431787cab42b
suppress some controls that don't work yet;

diff -r 47fb85ccfce8 -r d833cba5cce5 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Sun Jan 18 22:07:45 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Sun Jan 18 22:20:48 2015 +0100
@@ -83,9 +83,11 @@
       },
       graph_panel.zoom,
       new Button { action = Action("Fit to window") { graph_panel.fit_to_window() } },
-      new Button { action = Action("Update layout") { update_layout() } },
+      new Button { action = Action("Update layout") { update_layout() } })
+    /* FIXME
       new Button { action = Action("Colorations") { color_dialog.open } },
-      new Button { action = Action("Filters") { mutator_dialog.open } })
+      new Button { action = Action("Filters") { mutator_dialog.open } }
+    */
 
   layout(split_pane) = BorderPanel.Position.Center
   layout(controls) = BorderPanel.Position.North
diff -r 47fb85ccfce8 -r d833cba5cce5 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Sun Jan 18 22:07:45 2015 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Sun Jan 18 22:20:48 2015 +0100
@@ -149,7 +149,8 @@
   }
 
   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-    alphabetic, selection_label, selection_field, selection_apply)
+    // FIXME alphabetic,
+    selection_label, selection_field, selection_apply)
 
 
   /* main layout */