--- a/src/Tools/Graphview/main_panel.scala Sun Jan 18 17:34:14 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala Sun Jan 18 19:06:37 2015 +0100
@@ -33,7 +33,11 @@
graph_panel.refresh()
}
- val split_pane = new SplitPane(Orientation.Vertical, tree_panel, graph_panel)
+ val split_pane =
+ if (visualizer.get_options.bool("graphview_swap_panels"))
+ new SplitPane(Orientation.Vertical, tree_panel, graph_panel)
+ else
+ new SplitPane(Orientation.Vertical, graph_panel, tree_panel)
split_pane.oneTouchExpandable = true
val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false)