# HG changeset patch
# User wenzelm
# Date 1421604397 -3600
# Node ID 9f518fa77c1c40a50006af77aafa9b62478c0b8f
# Parent  02bacfc31446a4903339a7b06c34f63a8da78b0e
option graphview_swap_panels;

diff -r 02bacfc31446 -r 9f518fa77c1c src/Tools/Graphview/etc/options
--- a/src/Tools/Graphview/etc/options	Sun Jan 18 17:34:14 2015 +0100
+++ b/src/Tools/Graphview/etc/options	Sun Jan 18 19:06:37 2015 +0100
@@ -23,3 +23,6 @@
 public option graphview_content_margin : int = 60
   -- "margin for node content pretty-printing"
 
+public option graphview_swap_panels : bool = false
+  -- "swap panels for tree view versus graph layout"
+
diff -r 02bacfc31446 -r 9f518fa77c1c src/Tools/Graphview/main_panel.scala
--- 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)