# HG changeset patch
# User wenzelm
# Date 1421698530 -3600
# Node ID 0426b53a5d54b15d11bbe31c70233e3fc4ce631b
# Parent  99d009ede61954354b6cfe949bc37d17851905fc
always swap panels, which leads to slightly better GUI layout;

diff -r 99d009ede619 -r 0426b53a5d54 src/Tools/Graphview/etc/options
--- a/src/Tools/Graphview/etc/options	Mon Jan 19 21:06:47 2015 +0100
+++ b/src/Tools/Graphview/etc/options	Mon Jan 19 21:15:30 2015 +0100
@@ -23,6 +23,3 @@
 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 99d009ede619 -r 0426b53a5d54 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Mon Jan 19 21:06:47 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Mon Jan 19 21:15:30 2015 +0100
@@ -20,14 +20,8 @@
   val graph_panel = new Graph_Panel(visualizer)
   val tree_panel = new Tree_Panel(visualizer, graph_panel)
 
-  if (visualizer.options.bool("graphview_swap_panels")) {
-    leftComponent = tree_panel
-    rightComponent = graph_panel
-  }
-  else {
-    leftComponent = graph_panel
-    rightComponent = tree_panel
-  }
+  leftComponent = tree_panel
+  rightComponent = graph_panel
 
   def update_layout()
   {
diff -r 99d009ede619 -r 0426b53a5d54 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Mon Jan 19 21:06:47 2015 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Mon Jan 19 21:15:30 2015 +0100
@@ -87,7 +87,7 @@
   private val tree_pane = new ScrollPane(Component.wrap(tree))
   tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
   tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
-  tree_pane.minimumSize = new Dimension(100, 50)
+  tree_pane.minimumSize = new Dimension(100, 100)
   tree_pane.peer.getVerticalScrollBar.setUnitIncrement(10)