# HG changeset patch
# User wenzelm
# Date 1349700544 -7200
# Node ID 15e1549e6afe9072e6a8249d8810332a45a7df26
# Parent  38a68e6593be133a61d3bc43ebdea3e62a37bae0
tuned;

diff -r 38a68e6593be -r 15e1549e6afe src/Tools/Graphview/src/main_panel.scala
--- a/src/Tools/Graphview/src/main_panel.scala	Mon Oct 08 14:10:38 2012 +0200
+++ b/src/Tools/Graphview/src/main_panel.scala	Mon Oct 08 14:49:04 2012 +0200
@@ -14,10 +14,13 @@
 import scala.swing.{BorderPanel, Button, BoxPanel,
   Orientation, Swing, CheckBox, Action, FileChooser}
 
+import java.io.File
+import java.awt.{Color, Dimension}
+import java.awt.geom.Rectangle2D
+import java.awt.image.BufferedImage
+import javax.imageio.ImageIO
 import javax.swing.border.EmptyBorder
 import javax.swing.JComponent
-import java.awt.Dimension
-import java.io.File
 
 
 class Main_Panel(graph: Model.Graph)
@@ -115,11 +118,6 @@
   add(options_panel, BorderPanel.Position.North)
   
   private def export(file: File) {
-    import java.awt.image.BufferedImage
-    import javax.imageio.ImageIO
-    import java.awt.geom.Rectangle2D
-    import java.awt.Color    
-    
     val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds
     val img = new BufferedImage((math.abs(maxX - minX) + 400).toInt,
                                 (math.abs(maxY - minY) + 200).toInt,
@@ -132,10 +130,7 @@
     visualizer.Drawer.paint_all_visible(g, false)
     g.dispose()    
     
-    try {
-      ImageIO.write(img, "png", file)
-    } catch {
-      case ex: Exception => ex.printStackTrace
-    }  
+    try { ImageIO.write(img, "png", file) }
+    catch { case ex: Exception => ex.printStackTrace }  // FIXME !?
   }
 }