# HG changeset patch
# User wenzelm
# Date 1420120437 -3600
# Node ID 0df87ade7052465e4d2d590b7fd129d7090f1c61
# Parent  7b8c50be8d42389fca235cf2d960f20ef56cccac
more standard GUI layout;

diff -r 7b8c50be8d42 -r 0df87ade7052 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Thu Jan 01 14:40:20 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Thu Jan 01 14:53:57 2015 +0100
@@ -9,8 +9,7 @@
 
 import isabelle._
 
-import scala.swing.{BorderPanel, Button, BoxPanel,
-  Orientation, Swing, CheckBox, Action, FileChooser}
+import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser}
 
 import java.io.{File => JFile}
 import java.awt.{Color, Dimension, Graphics2D}
@@ -43,54 +42,44 @@
   chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
   chooser.title = "Save Image (.png or .pdf)"
 
-  val options_panel = new BoxPanel(Orientation.Horizontal) {
-    border = new EmptyBorder(0, 0, 10, 0)
-
-    contents += Swing.HGlue
-    contents += new CheckBox(){
-      selected = visualizer.arrow_heads
-      action = Action("Arrow Heads"){
-        visualizer.arrow_heads = selected
-        graph_panel.repaint()
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Save Image"){
-        chooser.showSaveDialog(this) match {
-          case FileChooser.Result.Approve => export(chooser.selectedFile)
-          case _ =>
+  val options_panel =
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+      new CheckBox() {
+        selected = visualizer.arrow_heads
+        action = Action("Arrow Heads") {
+          visualizer.arrow_heads = selected
+          graph_panel.repaint()
+        }
+      },
+      new Button {
+        action = Action("Save Image") {
+          chooser.showSaveDialog(this) match {
+            case FileChooser.Result.Approve => export(chooser.selectedFile)
+            case _ =>
+          }
         }
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += graph_panel.zoom
-
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Apply Layout"){
-        graph_panel.apply_layout()
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Fit to Window"){
-        graph_panel.fit_to_window()
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Colorations"){
-        color_dialog.open
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Filters"){
-        mutator_dialog.open
-      }
-    }
-  }
+      },
+      graph_panel.zoom,
+      new Button {
+        action = Action("Apply Layout") {
+          graph_panel.apply_layout()
+        }
+      },
+      new Button {
+        action = Action("Fit to Window") {
+          graph_panel.fit_to_window()
+        }
+      },
+      new Button {
+        action = Action("Colorations") {
+          color_dialog.open
+        }
+      },
+      new Button {
+        action = Action("Filters") {
+          mutator_dialog.open
+        }
+      })
 
   add(graph_panel, BorderPanel.Position.Center)
   add(options_panel, BorderPanel.Position.North)