--- 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 */