--- 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"
-
--- 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()
{
--- 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)