suppress some controls that don't work yet;
authorwenzelm
Sun, 18 Jan 2015 22:20:48 +0100
changeset 59400 d833cba5cce5
parent 59399 47fb85ccfce8
child 59401 6ee01e011976
suppress some controls that don't work yet;
src/Tools/Graphview/main_panel.scala
src/Tools/Graphview/tree_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
--- 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 */